take chained facts into consideration in tactic hammer (from Jasmin)

--- 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 ()