# HG changeset patch
# User desharna
# Date 1742912048 -3600
# Node ID ccc12a6dec138fbbc5c43103ef86e7334fb97e53
# Parent  56098b36c49f7a7305963b5901537b83dfe0393c
tuned to avoid list traversal and memory allocation

diff -r 56098b36c49f -r ccc12a6dec13 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Mar 25 13:42:15 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Mar 25 15:14:08 2025 +0100
@@ -370,10 +370,10 @@
   end
 
 fun fact_distinct eq facts =
-  fold (fn (i, fact as (_, th)) =>
+  fold_index (fn (i, fact as (_, th)) =>
       Net.insert_term_safe (eq o apply2 (normalize_eq o Thm.prop_of o snd o snd))
         (normalize_eq (Thm.prop_of th), (i, fact)))
-    (tag_list 0 facts) Net.empty
+    facts Net.empty
   |> Net.entries
   |> sort (int_ord o apply2 fst)
   |> map snd