clear_overloads : term_grammar.grammar -> term_grammar.grammar
STRUCTURE
SYNOPSIS
Remove non-trivial overloading from a term grammar
DESCRIPTION
For a term grammar tmG, clear_overloads tmG is the similar grammar, changed to remove non-trivial overloading. (Each constant remains overloaded with itself, which avoids the printing of the theory name for every constant).
USES
Sometimes overloading can be too helpful, when we would like to see the structure of a term (eg, in finding which theorems could simplify it).
EXAMPLE
In this example we obtain the current type and term grammars tyG and tmG, then reset the current grammars to be these, except with overloading cleared from the term grammar. We print some theorems (eg, to view their internal structure), and finally we reset the current grammars to the original ones.

> ratTheory.RATND_RAT_OF_NUM;
val it = |- (RATN (&n) = &n) /\ (RATD (&n) = 1): thm
> rich_listTheory.MEM_TAKE;
val it = |- !m l. m <= LENGTH l ==> !x. MEM x (TAKE m l) ==> MEM x l: thm

val (tyG, tmG) = Parse.current_grammars () ;
Parse.temp_set_grammars (tyG, term_grammar.clear_overloads tmG) ;

> ratTheory.RATND_RAT_OF_NUM;
val it = |- (RATN (rat_of_num n) = int_of_num n) /\ 
  (RATD (rat_of_num n) = 1n): thm
> rich_listTheory.MEM_TAKE;
val it = |- !m l.  m <= LENGTH l ==>
  !x. x IN LIST_TO_SET (TAKE m l) ==> x IN LIST_TO_SET l: thm

Parse.temp_set_grammars (tyG, tmG) ;
COMMENTS
To print just a few terms without overloading, print_without_macros may be easier.
SEEALSO
HOL  Kananaskis-13