merged

--- 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]));

--- 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;