--- 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
--- 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]);