src/ZF/OrdQuant.thy

--- a/src/ZF/OrdQuant.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/ZF/OrdQuant.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -382,9 +382,9 @@
 
 in
 
-val defREX_regroup = Simplifier.simproc @{theory}
+val defREX_regroup = Simplifier.simproc (the_context ())
   "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
-val defRALL_regroup = Simplifier.simproc @{theory}
+val defRALL_regroup = Simplifier.simproc (the_context ())
   "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
 
 end;