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