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.