src/HOL/Tools/simpdata.ML
changeset 32010 cb1a1c94b4cd
parent 30609 983e8b6e4e69
child 32149 ef59550a55d3
--- a/src/HOL/Tools/simpdata.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/simpdata.ML	Wed Jul 15 23:48:21 2009 +0200
@@ -181,11 +181,11 @@
   in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 val defALL_regroup =
-  Simplifier.simproc (the_context ())
+  Simplifier.simproc @{theory}
     "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
 
 val defEX_regroup =
-  Simplifier.simproc (the_context ())
+  Simplifier.simproc @{theory}
     "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;