parse_pretype : lexcode list -> pretype * lexcode list
Parses a pretype.
The call parse_pretype t, where t is a list of lexical tokens (as produced
by lex), parses the tokens and returns a pretype 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_preterm, parse_term, parse_type.