term_grammar

Parse.term_grammar : unit -> term_grammar.grammar

Returns the current global term grammar.

Failure

Never fails.

Comments

There is a pretty-printer installed in the interactive system so that term grammar values are presented nicely. The global term grammar is passed as a parameter to the Term parsing function in the Parse structure, and also drives the installed term and theorem pretty-printers.

See also

Parse.parse_from_grammars, Parse.print_from_grammars, Parse.temp_set_grammars, Parse.Term