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