diff -r b1af763166f4 -r a1f85f579a07 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 25 15:54:41 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 25 17:37:41 2025 +0100
@@ -44,7 +44,7 @@
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome ord
-  val one_line_proof_text : Proof.context -> int -> one_line_params -> string
+  val one_line_proof_text : one_line_params -> string
 end;
 
 structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
@@ -220,7 +220,7 @@
   | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
 
 (* FIXME *)
-fun proof_method_command meth i n used_chaineds _(*num_chained*) extras =
+fun proof_method_command meth i n used_chaineds extras =
   let
     val (indirect_facts, direct_facts) =
       if is_proof_method_direct meth then ([], extras) else (extras, [])
@@ -246,11 +246,10 @@
     (* Add optional markup break (command may need multiple lines) *)
     Markup.markup (Markup.break {width = 1, indent = 2}) " ")
 
-fun one_line_proof_text _ num_chained
-    ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
+fun one_line_proof_text ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
   let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
     map fst extra
-    |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
+    |> proof_method_command meth subgoal subgoal_count (map fst chained)
     |> (if play = Play_Failed then failed_command_line else try_command_line banner play)
   end