Primes a variable name sufficiently to make it distinct from all constants.
DESCRIPTION
When applied to a record made from a string v and a type ty, the
function mk_primed_var constructs a variable whose name consists of
v followed by however many primes are necessary to make it distinct
from any constants in the current theory.
FAILURE
Never fails.
EXAMPLE
- new_theory "wombat";
> val it = () : unit
- mk_primed_var("x", bool);
> val it = `x` : term
- new_constant("x", alpha);
> val it = () : unit
- mk_primed_var("x", bool);
> val it = `x'` : term