current_grammars
Parse.current_grammars : unit -> type_grammar.grammar * term_grammar.grammar
Obtains 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.Parse.current_grammars () returns the current values of these
grammars.
Failure
Never fails.
See also
Parse.temp_set_grammars,
Parse.term_grammar,
Parse.type_grammar