# HG changeset patch
# User desharna
# Date 1740501465 -3600
# Node ID c535cfba16db0644f09dda472102dcc435588dba
# Parent  a1f85f579a0727abdc2b9c59245eeed633759425
take chained facts into consideration in tactic hammer (from Jasmin)

diff -r a1f85f579a07 -r c535cfba16db src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Tue Feb 25 17:37:41 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Tue Feb 25 17:37:45 2025 +0100
@@ -86,11 +86,14 @@
   let
     val (basic_slice, No_Slice) = slice
     val facts = facts_of_basic_slice basic_slice factss
+    val {facts = chained, ...} = Proof.goal state
     val ctxt = Proof.context_of state
 
     val (local_facts, global_facts) =
-      fold (fn fact => if fst (snd (fst fact)) = Global then apsnd (cons (snd fact))
-        else apfst (cons (snd fact))) facts ([], [])
+      ([], [])
+      |> fold (fn fact => if fst (snd (fst fact)) = Global then apsnd (cons (snd fact))
+        else apfst (cons (snd fact))) facts
+      |> apfst (append chained)
 
     val timer = Timer.startRealTimer ()