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