variant : term list -> term -> term
STRUCTURE
SYNOPSIS
Modifies a variable name to avoid clashes.
DESCRIPTION
When applied to a list of variables to avoid clashing with, and a variable to modify, variant returns a variant of the variable to modify, that is, it changes the name as intuitively as possible to make it distinct from any variables in the list, or any constants. This is done by adding primes to the name.

The exact form of the variable name should not be relied on, except that the original variable will be returned unmodified unless it is itself in the list to avoid clashing with, or if it is the name of a constant.

FAILURE
variant l t fails if any term in the list l is not a variable or if t is not a variable.
EXAMPLE
The following shows a couple of typical cases:
   > variant [``y:bool``, ``z:bool``] ``x:bool``;
   val it = ``x`` : term

   > variant [``x:bool``, ``x':num``, ``x'':num``] ``x:bool``;
   > val it = ``x'''`` : term
while the following shows that clashes with the names of constants are also avoided:
   > variant [] (mk_var("T",bool));
   val it = ``T'`` : term
USES
The function variant is extremely useful for complicated derived rules which need to rename variables to avoid free variable capture while still making the role of the variable obvious to the user.
COMMENTS
There is a ‘Term.numvariant‘ function that has the same type signature, but which varies by adding and then incrementing a numeric suffix to the variable‚Äôs stem.
SEEALSO
HOL  Kananaskis-14