src/ZF/OrdQuant.thy

--- a/src/ZF/OrdQuant.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/ZF/OrdQuant.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -381,9 +381,9 @@
 
 in
 
-val defREX_regroup = Simplifier.simproc @{theory}
+val defREX_regroup = Simplifier.simproc_global @{theory}
   "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
-val defRALL_regroup = Simplifier.simproc @{theory}
+val defRALL_regroup = Simplifier.simproc_global @{theory}
   "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
 
 end;