variant : term list -> term -> term
Modifies a variable name to avoid clashes.
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.

variant l t fails if any term in the list l is not a variable or if t is not a variable.
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
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.
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.
HOL  Kananaskis-14