term_of_preterm : preterm -> term

SYNOPSIS
Converts a preterm into a term.

DESCRIPTION
HOL Light uses ``pretypes'' and ``preterms'' as intermediate structures for parsing and typechecking, which are later converted to types and terms. A call term_of_preterm ptm attempts to convert preterm ptm into a HOL term.

FAILURE CONDITIONS
Fails if some constants used in the preterm have not been defined, or if there are other inconsistencies in the types so that a consistent typing cannot be arrived at.

COMMENTS
Only users seeking to change HOL's parser and typechecker quite radically need to use this function.

SEE ALSO
preterm_of_term, retypecheck, type_of_pretype.