----------------------------------------------------------------------
current_grammars                                               (Parse)
----------------------------------------------------------------------
current_grammars : unit -> type_grammar.grammar * term_grammar.grammar

SYNOPSIS
Obtains the global type and term grammars.

DESCRIBE
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
Parse.temp_set_grammars, Parse.term_grammar, Parse.type_grammar.

----------------------------------------------------------------------