# HG changeset patch
# User paulson
# Date 1141121369 -3600
# Node ID f48e36b7d8d4ab47b0f575fbc3457772cc3e5c43
# Parent  0864119a961142f241e036de0adabde8bcec856b
fixed but in freeze_spec

diff -r 0864119a9611 -r f48e36b7d8d4 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue Feb 28 11:07:54 2006 +0100
+++ b/src/HOL/Tools/meson.ML	Tue Feb 28 11:09:29 2006 +0100
@@ -104,12 +104,6 @@
 (*number of literals in a term*)
 val nliterals = length o literals;
 
-(*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;
-
 
 (*** Tautology Checking ***)
 
@@ -166,13 +160,20 @@
 
 (*** 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 sth = th RS spec
+  let val names = add_term_names (prop_of th, [])
       val newname = (name_ref := !name_ref + 1;
-		     radixstring(26, "A", !name_ref))
-  in  read_instantiate [("x", newname)] sth  end;
+		     variant names (radixstring(26, "A", !name_ref)))
+      val spec' = read_instantiate [("x", newname)] spec
+  in  th RS spec'  end;
 
 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
   and then normalized via function nf. The normal form is given to resolve_tac,
@@ -202,12 +203,10 @@
 	  | Const ("op |", _) => (*disjunction*)
 	      let val tac =
 		  (METAHYPS (resop cnf_nil) 1) THEN
-		   (fn st' => st' |>  
-		      METAHYPS 
-		        (resop cnf_nil) 1)
+		   (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
 	      in  Seq.list_of (tac (th RS disj_forward)) @ ths  end 
 	  | _ => (*no work to do*) th::ths 
-      and cnf_nil th = (cnf_aux (th,[]))
+      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)