--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Sun Mar 30 13:50:06 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Mon Mar 31 09:30:44 2025 +0200
@@ -85,9 +85,6 @@
else if name = simpN then Simp_Method
else error ("Unknown tactic: " ^ quote name)
-fun tac_of ctxt name (local_facts, global_facts) =
- Sledgehammer_Proof_Methods.tac_of_proof_method ctxt (local_facts, global_facts) (meth_of name)
-
fun run_tactic_prover mode name ({slices, timeout, ...} : params)
({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =
let