parse_preterm : lexcode list -> preterm * lexcode list
Parses a preterm.
The call parse_preterm t, where t is a list of lexical tokens (as produced
by lex), parses the tokens and returns a preterm as well as the unparsed
- FAILURE CONDITIONS
Fails if there is a syntax error in the token list.
This is mostly an internal function; pretypes and preterms are used as an
intermediate representation for typechecking and overload resolution and are
not normally of concern to users.
- SEE ALSO
lex, parse_pretype, parse_term, parse_type.