--- a/src/FOL/FOL.thy Sun May 24 21:11:23 2020 +0200
+++ b/src/FOL/FOL.thy Sun May 24 19:57:13 2020 +0000
@@ -337,8 +337,8 @@
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>fn _ => Quantifier1.rearrange_Ex\<close>
+simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_All\<close>
ML \<open>
(*intuitionistic simprules only*)