# 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;