# HG changeset patch
# User desharna
# Date 1742919096 -3600
# Node ID 541370cb289dad071910bfa08131db3f712cad3c
# Parent  b1c40a1ae4a932db3e63d59b17497f902c025f71
tuned

diff -r b1c40a1ae4a9 -r 541370cb289d src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Mar 25 15:26:48 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Mar 25 17:11:36 2025 +0100
@@ -489,7 +489,7 @@
                 NONE => false
               | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths'))
           in
-            snd (fold_rev (fn th0 => fn (j, accum) =>
+            snd (fold_rev (fn th0 => fn (j, accum as {singletons, dotteds, collections}) =>
               let val th = transfer th0 in
                 (j - 1,
                  if not (member Thm.eq_thm_prop add_ths th) andalso
@@ -517,19 +517,23 @@
                      val stature = stature_of_thm global assms chained css name0 th
                      val new = ((get_name, stature), th)
                    in
-                     (if collection then apsnd o apsnd
-                      else if dotted_name then apsnd o apfst
-                      else apfst) (cons new) accum
+                     if collection then
+                       {singletons = singletons, dotteds = dotteds, collections = new :: collections}
+                      else if dotted_name then
+                       {singletons = singletons, dotteds = new :: dotteds, collections = collections}
+                      else
+                       {singletons = new :: singletons, dotteds = dotteds, collections = collections}
                    end)
               end) ths (n, accum))
           end)
+      val {singletons, dotteds, collections} =
+        {singletons = [], dotteds = [], collections = []}
+        |> add_facts false fold local_facts (unnamed_locals @ named_locals)
+        |> add_facts true Facts.fold_static global_facts global_facts
   in
     (* Names like "xxx" are preferred to "xxx.yyy", which are preferred to "xxx(666)" and the like.
        "Preferred" means "put to the front of the list". *)
-    ([], ([], []))
-    |> add_facts false fold local_facts (unnamed_locals @ named_locals)
-    |> add_facts true Facts.fold_static global_facts global_facts
-    ||> op @ |> op @
+    singletons @ dotteds @ collections
   end
 
 fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts concl_t =