src/HOL/Set.thy

--- a/src/HOL/Set.thy	Thu Dec 01 22:03:06 2005 +0100
+++ b/src/HOL/Set.thy	Thu Dec 01 22:04:27 2005 +0100
@@ -426,24 +426,17 @@
 
 ML_setup {*
   local
-    val Ball_def = thm "Ball_def";
-    val Bex_def = thm "Bex_def";
-
-    val simpset = Simplifier.clear_ss HOL_basic_ss;
-    fun unfold_tac ss th =
-      ALLGOALS (full_simp_tac (Simplifier.inherit_context ss simpset addsimps [th]));
-
-    fun prove_bex_tac ss =
-      unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac;
+    val unfold_bex_tac = unfold_tac [thm "Bex_def"];
+    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
     val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
 
-    fun prove_ball_tac ss =
-      unfold_tac ss Ball_def THEN Quantifier1.prove_one_point_all_tac;
+    val unfold_ball_tac = unfold_tac [thm "Ball_def"];
+    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
     val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
   in
-    val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+    val defBEX_regroup = Simplifier.simproc (the_context ())
       "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
-    val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+    val defBALL_regroup = Simplifier.simproc (the_context ())
       "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
   end;