1.1 --- a/src/HOL/Tools/meson.ML	Thu May 25 16:51:39 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri May 26 22:20:02 2006 +0200
     1.3 @@ -159,18 +159,10 @@
     1.4  
     1.5  (*** The basic CNF transformation ***)
     1.6  
     1.7 -(*Generation of unique names -- maxidx cannot be relied upon to increase!
     1.8 -  Cannot rely on "variant", since variables might coincide when literals
     1.9 -  are joined to make a clause...
    1.10 -  19 chooses "U" as the first variable name*)
    1.11 -val name_ref = ref 19;
    1.12 -
    1.13  (*Replaces universally quantified variables by FREE variables -- because
    1.14    assumptions may not contain scheme variables.  Later, call "generalize". *)
    1.15  fun freeze_spec th =
    1.16 -  let val names = add_term_names (prop_of th, [])
    1.17 -      val newname = (name_ref := !name_ref + 1;
    1.18 -		     variant names (radixstring(26, "A", !name_ref)))
    1.19 +  let val newname = gensym "A_"
    1.20        val spec' = read_instantiate [("x", newname)] spec
    1.21    in  th RS spec'  end;
    1.22  
    1.23 @@ -207,7 +199,6 @@
    1.24  	  | _ => (*no work to do*) th::ths 
    1.25        and cnf_nil th = cnf_aux (th,[])
    1.26    in 
    1.27 -    name_ref := 19;  (*It's safe to reset this in a top-level call to cnf*)
    1.28      cnf_aux (th,ths)
    1.29    end;
    1.30