parse_from_grammars :
  (type_grammar.grammar * term_grammar.grammar) ->
  ((hol_type frag list -> hol_type) * (term frag list -> term))
STRUCTURE
SYNOPSIS
Returns parsing functions based on the supplied grammars.
DESCRIPTION
When given a pair consisting of a type and a term grammar, this function returns parsing functions that use those grammars to turn strings (strictly, quotations) into types and terms respectively.
FAILURE
Can’t fail immediately. However, when the precedence matrix for the term parser is built on first application of the term parser, this may generate precedence conflict errors depending on the rules in the grammar.
EXAMPLE
First the user loads arithmeticTheory to augment the built-in grammar with the ability to lex numerals and deal with symbols such as + and -:
   - load "arithmeticTheory";
   > val it = () : unit
   - val t = Term`2 + 3`;
   > val t = `2 + 3` : term
Then the parse_from_grammars function is used to make the values Type and Term use the grammar present in the simpler theory of booleans. Using this function fails to parse numerals or even the + infix:
   - val (Type,Term) = parse_from_grammars boolTheory.bool_grammars;
   > val Type = fn : hol_type frag list -> hol_type
     val Term = fn : term frag list -> term
   - Term`2 + 3`;
   <<HOL message: No numerals currently allowed.>>
   ! Uncaught exception:
   ! HOL_ERR <poly>
   - Term`x + y`;
   <<HOL message: inventing new type variable names: 'a, 'b.>>
   > val it = `x $+ y` : term
But, as the last example above also demonstrates, the installed pretty-printer is still dependent on the global grammar, and the global value of Term can still be accessed through the Parse structure:
   - t;
   > val it = `2 + 3` : term

   - Parse.Term`2 + 3`;
   > val it = `2 + 3` : term

USES
This function is used to ensure that library code has access to a term parser that is a known quantity. In particular, it is not good form to have library code that depends on the default parsers Term and Type. When the library is loaded, which may happen at any stage, these global values may be such that the parsing causes quite unexpected results or failures.
SEEALSO
HOL  Trindemossen-1