# HG changeset patch
# User desharna
# Date 1742912808 -3600
# Node ID b1c40a1ae4a932db3e63d59b17497f902c025f71
# Parent  d935fa3b90f241f02dd5fc921c6330e3ad797932
tuned to avoid list traversal and memory allocation

diff -r d935fa3b90f2 -r b1c40a1ae4a9 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Mar 25 15:24:30 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Mar 25 15:26:48 2025 +0100
@@ -175,8 +175,8 @@
         ()
 
     fun print_used_facts used_facts used_from =
-      tag_list 1 used_from
-      |> map (fn (j, fact) => fact |> apsnd (K j))
+      used_from
+      |> map_index (fn (j, fact) => fact |> apsnd (K (j + 1)))
       |> filter_used_facts false used_facts
       |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
       |> commas
@@ -188,8 +188,8 @@
           val num_used_facts = length used_facts
 
           fun find_indices facts =
-            tag_list 1 facts
-            |> map (fn (j, fact) => fact |> apsnd (K j))
+            facts
+            |> map_index (fn (j, fact) => fact |> apsnd (K (j + 1)))
             |> filter_used_facts false used_facts
             |> distinct (eq_fst (op =))
             |> map (prefix "@" o string_of_int o snd)