temp_set_grammars : type_grammar.grammar * term_grammar.grammar -> unit
STRUCTURE
SYNOPSIS
Sets the global type and term grammars.
DESCRIPTION
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
HOL  Trindemossen-1