remove_ovl_mapping
Parse.remove_ovl_mapping: string -> {Name:string,Thy:string} -> unit
Removes an overloading mapping between the string and constant specified.
Each grammar maintains two maps internally. One is from strings to non-empty lists of terms, and the other is from terms to strings. The first map is used to resolve overloading when parsing. A string will eventually be turned into one of the terms in the list that it maps to. When printing a constant, the map in the opposite direction is used to turn a term into a string.
A call to remove_ovl_mapping s {Name,Thy}, maps the Name-Thy
record to a constant c, and removes the c-s pair from both maps.
Failure
Never fails. If the given pair is not in either map, the function silently does nothing.
To prune the overloading maps of unwanted possibilities.
Comments
Note that removing a print-mapping for a constant will result in that
constant always printing fully qualified as thy$name. This situation
will persist until that constant is given a name to map to (either with
overload_on or update_overload_maps).
As with other parsing functions, there is a sister function,
temp_remove_ovl_mapping that does the same thing, but whose effect is
not saved to a theory file.
See also
Parse.clear_overloads_on,
Parse.overload_on,
Parse.update_overload_maps