# HG changeset patch
# User haftmann
# Date 1583263583 0
# Node ID 7807d828a0613aeeca51c9ffff0034c9c8485090
# Parent  a57413dd2909cc2150645168595ee60c332d101c
tuned

diff -r a57413dd2909 -r 7807d828a061 src/HOL/HOL.thy
--- 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>