1\DOC term_grammar 2 3\TYPE {Parse.term_grammar : unit -> term_grammar.grammar} 4 5\SYNOPSIS 6Returns the current global term grammar. 7 8\KEYWORDS 9Parsing, pretty-printing 10 11\LIBRARY 12Parse 13 14\FAILURE 15Never fails. 16 17\COMMENTS 18There is a pretty-printer installed in the interactive system so that 19term grammar values are presented nicely. The global term grammar is 20passed as a parameter to the {Term} parsing function in the {Parse} 21structure, and also drives the installed term and theorem 22pretty-printers. 23 24\SEEALSO 25Parse.parse_from_grammars, Parse.print_from_grammars, 26Parse.temp_set_grammars, Parse.Term. 27\ENDDOC 28