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