# HG changeset patch
# User haftmann
# Date 1591284622 0
# Node ID b0da0537f3077c15c378394f8101f668cc7e81bf
# Parent  2e7df6774373015ced80571b5faee7b0ad67f2e5
activate simproc for FOL

diff -r 2e7df6774373 -r b0da0537f307 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Thu Jun 04 15:30:22 2020 +0000
+++ b/src/FOL/FOL.thy	Thu Jun 04 15:30:22 2020 +0000
@@ -337,8 +337,9 @@
 
 ML_file \<open>simpdata.ML\<close>
 
-simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_Ex\<close>
-simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_All\<close>
+simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>K Quantifier1.rearrange_Ex\<close>
+simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>K Quantifier1.rearrange_All\<close>
+simproc_setup defined_all("\<And>x. PROP P(x)") = \<open>K Quantifier1.rearrange_all\<close>
 
 ML \<open>
 (*intuitionistic simprules only*)