temp_set_grammars
Parse.temp_set_grammars : type_grammar.grammar * term_grammar.grammar -> unit
Sets the global type and term grammars.
HOL uses two global grammars to control the parsing and printing of term
and type values. These can be adjusted in a controlled way with
functions such as add_rule and overload_on. By using just these
standard functions, the system is able to export theories in such a way
that changes to grammars persist from session to session.
Nonetheless it is occasionally useful to set grammar values directly. This change can't be made to persist, but will affect the current session.
Failure
Never fails.
See also
Parse.current_grammars,
Parse.add_rule,
Parse.overload_on,
Parse.parse_from_grammars,
Parse.print_from_grammars,
Parse.Term