--- a/src/HOL/HOL.thy Wed Mar 04 15:38:02 2020 +0100
+++ b/src/HOL/HOL.thy Tue Mar 03 19:26:23 2020 +0000
@@ -1215,8 +1215,8 @@
Simplifier.method_setup Splitter.split_modifiers
\<close>
-simproc_setup defined_Ex ("\<exists>x. P x") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
-simproc_setup defined_All ("\<forall>x. P x") = \<open>fn _ => Quantifier1.rearrange_all\<close>
+simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_ex\<close>
+simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_all\<close>
text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>