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