--- a/src/HOL/Tools/simpdata.ML Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Wed Aug 25 18:36:22 2010 +0200
@@ -182,11 +182,11 @@
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
val defALL_regroup =
- Simplifier.simproc @{theory}
+ Simplifier.simproc_global @{theory}
"defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
val defEX_regroup =
- Simplifier.simproc @{theory}
+ Simplifier.simproc_global @{theory}
"defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;