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