# HG changeset patch
# User wenzelm
# Date 1245094407 -7200
# Node ID 76d8c30a92c5a96ca0534757a1a3a9564c965472
# Parent  f4723b1ae5a14da57ef9dd8c5d25ef4c72a210cb# Parent  ef30cd0e41e5f9f2c240c1f8fdfdc8a416c6b915
merged

diff -r f4723b1ae5a1 -r 76d8c30a92c5 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Mon Jun 15 21:28:04 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Jun 15 21:33:27 2009 +0200
@@ -212,7 +212,7 @@
         fun prove_eqs aux_simp proj_defs lthy = 
           let
             val proj_simps = map (snd o snd) proj_defs;
-            fun tac { context = ctxt, ... } =
+            fun tac { context = ctxt, prems = _ } =
               ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
               THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
               THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
diff -r f4723b1ae5a1 -r 76d8c30a92c5 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Mon Jun 15 21:28:04 2009 +0200
+++ b/src/Pure/pure_setup.ML	Mon Jun 15 21:33:27 2009 +0200
@@ -4,15 +4,6 @@
 Pure theory and ML toplevel setup.
 *)
 
-(* ML toplevel use commands *)
-
-fun use name          = Toplevel.program (fn () => ThyInfo.use name);
-fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
-fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
-fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
-fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
-
-
 (* the Pure theories *)
 
 val theory = ThyInfo.get_theory;
@@ -49,6 +40,15 @@
 else ();
 
 
+(* ML toplevel use commands *)
+
+fun use name          = Toplevel.program (fn () => ThyInfo.use name);
+fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
+fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
+fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
+fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
+
+
 (* misc *)
 
 val cd = File.cd o Path.explode;