# HG changeset patch
# User desharna
# Date 1743176278 -3600
# Node ID 2db8a047b52c772f0f5b2978fb2effaea00761ef
# Parent  971613edfb9482a150df579efddf758b7e53665e
tuned

diff -r 971613edfb94 -r 2db8a047b52c src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Fri Mar 28 16:20:48 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Fri Mar 28 16:37:58 2025 +0100
@@ -97,13 +97,9 @@
 
     fun run_try0 () : Try0.result option =
       let
-        val _ = Proof_Context.get_fact
-        val _ = Args.named_fact
-        val _ = Pretty.pure_string_of
-        val _ = Thm.pretty_thm
         val run_timeout = slice_timeout slice_size slices timeout
         fun is_cartouche str = String.isPrefix "\<open>" str andalso String.isSuffix "\<close>" str
-        fun xref_of_fact (((name, (_, status)), thm) : Sledgehammer_Fact.fact) =
+        fun xref_of_fact (((name, _), thm) : Sledgehammer_Fact.fact) =
             let
               val xref =
                 if is_cartouche name then