--- 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*)