--- 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