The flag Globals.priming controls how certain system function perform
renaming of variables. When priming has the value NONE, renaming
is achieved by concatenation of primes ('). When priming has the
value SOME s, renaming is achieved by incrementing a counter.
The default value of priming is NONE.
EXAMPLE
- mk_primed_var ("T",bool);
> val it = `T'` : term
- with_flag (priming,SOME "_") mk_primed_var ("T",bool);
> val it = `T_1` : term
COMMENTS
Proofs should be re-run in the same priming regime as they were
originally performed in, since different styles of renaming can
break proofs.