----------------------------------------------------------------------
clear_overloads_on                                             (Parse)
----------------------------------------------------------------------
Parse.clear_overloads_on : string -> unit

SYNOPSIS
Clears all overloading on the specified operator.

KEYWORDS
Parsing, pretty-printing, overloading.

LIBRARY
Parse

DESCRIBE
This function removes all overloading associated with the given
string, except those "overloads" that map the string to constants of
the same name.  These additional overloads (there may be more than one
constant of the same name, as long as each such is part of a different
theory) may be removed with {remove_ovl_mapping}, or by using {hide}.

FAILURE
Never fails.  If a string is not overloaded, this function simply has
no effect.

EXAMPLE

- load "realTheory";
> val it = () : unit
- realTheory.REAL_INV_LT1;
> val it = |- !x. 0 < x /\ x < 1 ==> 1 < inv x : thm
- clear_overloads_on "<";
> val it = () : unit
- realTheory.REAL_INV_LT1;
> val it = |- !x. 0 real_lt x /\ x real_lt 1 ==> 1 real_lt inv x : thm
- clear_overloads_on "&";
> val it = () : unit
- realTheory.REAL_INV_LT1;
> val it = |- !x. 0r real_lt x /\ x real_lt 1r ==> 1r real_lt inv x : thm




USES
If overloading gets too confusing, this function should help to clear
away one layer of supposedly helpful obfuscation.

COMMENTS
As with other parsing functions, there is a sister function,
{temp_clear_overloads_on} that does the same thing, but whose effect
is not saved to a theory file.

SEEALSO
Parse.overload_on, Parse.remove_ovl_mapping.

----------------------------------------------------------------------