remove_interface : string -> unit

SYNOPSIS
Remove all overload/interface mappings for an identifier.

DESCRIPTION
HOL Light allows an identifier to map to a specific constant (see override_interface) or be overloaded to several depending on type (see overload_interface). A call to remove_interface "ident" removes all such mappings for the identifier ident.

FAILURE CONDITIONS
Never fails, whether or not there were any interface mappings in effect.

SEE ALSO
overload_interface, override_interface, reduce_interface, the_interface.