parse_pretype : lexcode list -> pretype * lexcode list

SYNOPSIS: Parses a pretype.
DESCRIPTION: 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 tokens.
FAILURE CONDITIONS: Fails if there is a syntax error in the token list.
USES: 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.