functional theory setup -- requires linear access;

--- a/src/ZF/simpdata.ML	Sat Mar 29 22:56:00 2008 +0100
+++ b/src/ZF/simpdata.ML	Sat Mar 29 22:56:01 2008 +0100
@@ -61,10 +61,10 @@
 
 in
 
-val defBEX_regroup = Simplifier.simproc @{theory}
+val defBEX_regroup = Simplifier.simproc (Theory.deref @{theory_ref})
   "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
 
-val defBALL_regroup = Simplifier.simproc @{theory}
+val defBALL_regroup = Simplifier.simproc (Theory.deref @{theory_ref})
   "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
 
 end;