--- a/src/ZF/simpdata.ML Thu Oct 28 22:59:33 2010 +0200
+++ b/src/ZF/simpdata.ML Thu Oct 28 23:19:52 2010 +0200
@@ -59,10 +59,10 @@
in
-val defBEX_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
+val defBEX_regroup = Simplifier.simproc_global @{theory}
"defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
-val defBALL_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
+val defBALL_regroup = Simplifier.simproc_global @{theory}
"defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
end;