freeze_spec: gensym;
authorwenzelm
Fri, 26 May 2006 22:20:02 +0200
changeset 19728 6c47d9295dca
parent 19727 f5895f998402
child 19729 cb9e2f0c7658
freeze_spec: gensym;
src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu May 25 16:51:39 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Fri May 26 22:20:02 2006 +0200
@@ -159,18 +159,10 @@
 
 (*** The basic CNF transformation ***)
 
-(*Generation of unique names -- maxidx cannot be relied upon to increase!
-  Cannot rely on "variant", since variables might coincide when literals
-  are joined to make a clause...
-  19 chooses "U" as the first variable name*)
-val name_ref = ref 19;
-
 (*Replaces universally quantified variables by FREE variables -- because
   assumptions may not contain scheme variables.  Later, call "generalize". *)
 fun freeze_spec th =
-  let val names = add_term_names (prop_of th, [])
-      val newname = (name_ref := !name_ref + 1;
-		     variant names (radixstring(26, "A", !name_ref)))
+  let val newname = gensym "A_"
       val spec' = read_instantiate [("x", newname)] spec
   in  th RS spec'  end;
 
@@ -207,7 +199,6 @@
 	  | _ => (*no work to do*) th::ths 
       and cnf_nil th = cnf_aux (th,[])
   in 
-    name_ref := 19;  (*It's safe to reset this in a top-level call to cnf*)
     cnf_aux (th,ths)
   end;