current_grammars : unit -> type_grammar.grammar * term_grammar.grammar
STRUCTURE
SYNOPSIS
Obtains 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. Parse.current_grammars () returns the current values of these grammars.
FAILURE
Never fails.
SEEALSO
HOL  Trindemossen-1