----------------------------------------------------------------------
temp_set_grammars                                              (Parse)
----------------------------------------------------------------------
temp_set_grammars : type_grammar.grammar * term_grammar.grammar -> unit

SYNOPSIS
Sets the global type and term grammars.

DESCRIBE
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.

SEEALSO
Parse.current_grammars, Parse.add_rule, Parse.overload_on,
Parse.parse_from_grammars, Parse.print_from_grammars, Parse.Term.

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