parse_term : string -> term
Parses a string into a HOL term.
The call parse_term "s" parses the string s into a HOL term. This is the
function that is invoked automatically when a term is written in quotations
- FAILURE CONDITIONS
Fails in the event of a syntax error or unparsed input.
# parse_term "p /\\ q ==> r";;
val it : term = `p /\ q ==> r`
Note that backslash characters should be doubled up when entering OCaml
strings, as in the example above, since they are the string escape character.
This is handled automatically by the quotation parser, so one doesn't need to
do it (indeed shouldn't do it) when entering quotations between backquotes.
- SEE ALSO