# HG changeset patch
# User wenzelm
# Date 1634412015 -7200
# Node ID 7d05d44ff9a9cb2ef30f30e99984fbd72e6b9ccd
# Parent  2f8e8dc9b5224def4439e739af52fdc4c84ccf0d
clarified context;

diff -r 2f8e8dc9b522 -r 7d05d44ff9a9 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Oct 16 21:15:28 2021 +0200
+++ b/src/HOL/HOL.thy	Sat Oct 16 21:20:15 2021 +0200
@@ -2104,9 +2104,9 @@
 method_setup eval = \<open>
   let
     fun eval_tac ctxt =
-      let val conv = Code_Runtime.dynamic_holds_conv ctxt
+      let val conv = Code_Runtime.dynamic_holds_conv
       in
-        CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
+        CONVERSION (Conv.params_conv ~1 (Conv.concl_conv ~1 o conv) ctxt) THEN'
         resolve_tac ctxt [TrueI]
       end
   in
diff -r 2f8e8dc9b522 -r 7d05d44ff9a9 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Oct 16 21:15:28 2021 +0200
+++ b/src/Tools/induct.ML	Sat Oct 16 21:20:15 2021 +0200
@@ -444,8 +444,8 @@
 val equal_def' = Thm.symmetric Induct_Args.equal_def;
 
 fun mark_constraints n ctxt = Conv.fconv_rule
-  (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n
-     (Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt));
+  (Conv.prems_conv ~1 (Conv.params_conv ~1 (fn ctxt' =>
+      Conv.prems_conv n (Raw_Simplifier.rewrite ctxt' false [equal_def'])) ctxt));
 
 fun unmark_constraints ctxt =
   Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]);