term_of_preterm : preterm -> term
Converts a preterm into a term.
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
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.