Replace a theorem’s type variables with fresh versions
DESCRIPTION
A call to FULL_GEN_TYVARIFTY th replaces (with INST_TYPE) the type
variables occurring in theorem th. 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 GEN_TYVARIFY will only instantiate those type
variables that are exclusively found in the conclusion. This is
reasonable when handling theorems derived from a tactic goal’s
assumptions.