print_without_macros : term -> unit
STRUCTURE
Parse
SYNOPSIS
Prints a term to standard output, using the current grammars but without non-trivial overloading
DESCRIPTION
Where print_term uses the (implicit) global grammars to control the printing of its term argument, the print_without_macros uses these grammars, modified to remove non-trivial overloading. (Each constant is overloaded with itself, which avoids the printing of the theory name for every constant).
FAILURE
Never fails.
USES
Sometimes one wants to see how a term is built up, where the pretty-printing simplifies it to the point where this is not clear.

For example: 

``MEM`` ;
val it = ``\x l. MEM x l`` ;
print_without_macros ``MEM`` ;
 \x l. x IN LIST_TO_SET l

concl ratTheory.RATND_RAT_OF_NUM ;
val it = (RATN (&n) = &n) /\ (RATD (&n) = 1): term
Parse.print_without_macros (concl ratTheory.RATND_RAT_OF_NUM) ;
(RATN (rat_of_num n) = int_of_num n) /\ (RATD (rat_of_num n) = 1n)
COMMENTS
To change the (implicit) global grammars to remove overloading, see clear_overloads
SEEALSO
print_term_by_grammar, clear_overloads
HOL  Trindemossen-1