diff -r c535cfba16db -r c819ee4cdea9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Tue Feb 25 17:37:45 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Tue Feb 25 17:41:52 2025 +0100
@@ -79,10 +79,8 @@
   else
     error ("Unknown tactic: " ^ quote name)
 
-fun run_tactic_prover mode name (params as {debug, verbose, isar_proofs, compress, try0, minimize,
-     timeout, ...})
-    ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem)
-    slice =
+fun run_tactic_prover mode name ({timeout, ...} : params)
+    ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =
   let
     val (basic_slice, No_Slice) = slice
     val facts = facts_of_basic_slice basic_slice factss