# HG changeset patch
# User desharna
# Date 1743440304 -7200
# Node ID 381970dd5b21e93680f8eae54a907d533acdfa12
# Parent  44440263d847e479fb03fe2a710bb9f321d56db7
tuned

diff -r 44440263d847 -r 381970dd5b21 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Mon Mar 31 18:55:45 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Mon Mar 31 18:58:24 2025 +0200
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
     Author:     Jasmin Blanchette, LMU Muenchen
+    Author:     Martin Desharnais, LMU Muenchen
 
 Isabelle tactics as Sledgehammer provers.
 *)
@@ -19,9 +20,7 @@
 structure Sledgehammer_Prover_Tactic : SLEDGEHAMMER_PROVER_TACTIC =
 struct
 
-open ATP_Problem_Generate
 open ATP_Proof
-open Sledgehammer_ATP_Systems
 open Sledgehammer_Proof_Methods
 open Sledgehammer_Prover
 
@@ -52,7 +51,7 @@
   | meth_of _ = Metis_Method (NONE, NONE, [])
 
 fun run_tactic_prover mode name ({slices, timeout, ...} : params)
-    ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =
+    ({state, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =
   let
     val (basic_slice as (slice_size, _, _, _, _), No_Slice) = slice
     val facts = facts_of_basic_slice basic_slice factss