Replace a theorem’s type variables with fresh versions
DESCRIPTION
A call to GEN_TYVARIFY th replaces (with INST_TYPE) the type
variables occurring in theorem th’s conclusion that do not also
appear in any of th’s hypotheses. The new type variables are
generated by successive calls to gen_tyvar, so should not have been
seen before.
FAILURE
Never fails.
COMMENTS
The derived rule FULL_GEN_TYVARIFY will instantiate all of a
theorem’s type variables, whether or not they appear in the
hypotheses.