prim_variant
Term.prim_variant : term list -> term -> term
Rename a variable to be different from any in a list.
The function prim_variant is exactly the same as variant, except
that it doesn't rename away from constants.
Failure
prim_variant l t fails if any term in the list l is not a variable
or if t is not a variable.
Example
> variant [] (mk_var("T",bool));
val it = “T'”: term
> prim_variant [] (mk_var("T",bool));
val it = “T”: term
Comments
The extra amount of renaming that variant does is useful when
generating new constant names (even though it returns a variable) inside
high-level definition mechanisms. Otherwise, prim_variant seems
preferable.