delete_parser : string -> unit

SYNOPSIS
Uninstall a user parser.

DESCRIPTION
HOL Light allows user parsing functions to be installed, and will try them on all terms during parsing before the usual parsers. The call delete_parser "s" removes any parsers associated with string "s".

FAILURE CONDITIONS
Never fails, regardless of whether there are any parsers associated with the string.

SEE ALSO
install_parser, installed_parsers, try_user_parser.