Rename a variable to be different from any in a list.
DESCRIPTION
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.