# HG changeset patch
# User desharna
# Date 1743406244 -7200
# Node ID dd427ae513e2a2fc586b0263a02327e2ad399b5a
# Parent  ceb4f33d30736de7ac6f58d8941c1db756511c70
removed unused function

diff -r ceb4f33d3073 -r dd427ae513e2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- 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