# HG changeset patch
# User wenzelm
# Date 1206827761 -3600
# Node ID b4db4e1657588b2f9084e97643874497acab1d2a
# Parent  3f0231b880a7802ae9df39e91d9a5899277dfa17
functional theory setup -- requires linear access;

diff -r 3f0231b880a7 -r b4db4e165758 src/ZF/simpdata.ML
--- 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;