--- a/src/ZF/simpdata.ML Wed Aug 25 18:19:04 2010 +0200
+++ b/src/ZF/simpdata.ML Wed Aug 25 18:36:22 2010 +0200
@@ -59,10 +59,10 @@
in
-val defBEX_regroup = Simplifier.simproc (Theory.deref @{theory_ref})
+val defBEX_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
"defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
-val defBALL_regroup = Simplifier.simproc (Theory.deref @{theory_ref})
+val defBALL_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
"defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
end;