variants : term list -> term list -> term list

SYNOPSIS
Pick a list of variants of variables, avoiding a list of variables and each other.

DESCRIPTION
The call variants av vs,s where av and vs are both lists of variables, will return a list vs' of variants of the variables in the list vs, renamed as necessary by adding primes to avoid clashing with any free variables of the terms in the list av or with each other.

FAILURE CONDITIONS
Fails if any of the terms in the list is not a variable.

EXAMPLE
  # variants [`x':num`; `x'':num`; `y:bool`] [`x:num`; `x':num`];;
  val it : term list = [`x`; `x'''`]

SEE ALSO
genvar, mk_primed_var, variant.