diff -r 1f46f6f7dec4 -r 14a28584e759 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 12:46:50 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 12:50:46 2025 +0100
@@ -368,15 +368,15 @@
       | process (#"A", [_, t]) tstate =
           gettm t tstate |>> Thm.apply \<^cterm>\<open>Trueprop\<close> |>> Skip_Proof.make_thm_cterm |-> setth
       | process (#"C", [th1, th2]) tstate =
-          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => comb t1 t2) |-> setth
+          getth th1 tstate ||>> getth th2 |>> uncurry comb |-> setth
       | process (#"T", [th1, th2]) tstate =
-          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => trans t1 t2) |-> setth
+          getth th1 tstate ||>> getth th2 |>> uncurry trans |-> setth
       | process (#"E", [th1, th2]) tstate =
-          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => eq_mp t1 t2) |-> setth
+          getth th1 tstate ||>> getth th2 |>> uncurry eq_mp |-> setth
       | process (#"D", [th1, th2]) tstate =
-          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => deduct t1 t2) |-> setth
+          getth th1 tstate ||>> getth th2 |>> uncurry deduct |-> setth
       | process (#"L", [t, th]) tstate =
-          gettm t tstate ||>> (fn ti => getth th ti) |>> (fn (tm, th) => abs tm th) |-> setth
+          gettm t tstate ||>> (fn ti => getth th ti) |>> uncurry abs |-> setth
       | process (#"M", [s]) (thy, state) =
           let
             val ctxt = Proof_Context.init_global thy
@@ -429,9 +429,9 @@
       | process (#"c", [n, ty]) (thy, state) =
           getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (make_const thy (n, Thm.typ_of ty))) |-> settm
       | process (#"f", [t1, t2]) tstate =
-          gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.apply t1 t2) |-> settm
+          gettm t1 tstate ||>> gettm t2 |>> uncurry Thm.apply |-> settm
       | process (#"l", [t1, t2]) tstate =
-          gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.lambda t1 t2) |-> settm
+          gettm t1 tstate ||>> gettm t2 |>> uncurry Thm.lambda |-> settm
       | process (#"+", [s]) (thy, state) =
           (store_thm (Binding.name (make_name s)) (last_thm state) thy, state)
       | process (c, _) _ = error ("process: unknown command: " ^ String.implode [c])