# HG changeset patch
# User wenzelm
# Date 1729863567 -7200
# Node ID 1c2be1fca2bda8bd7875c93011e047d357b04b38
# Parent  74647c464cbdd2eb827289213b279157a087b792
minor performance tuning;

diff -r 74647c464cbd -r 1c2be1fca2bd src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Fri Oct 25 13:43:12 2024 +0200
+++ b/src/Pure/term_items.ML	Fri Oct 25 15:39:27 2024 +0200
@@ -224,6 +224,13 @@
 end;
 
 
+structure Indexnames: TERM_ITEMS = Term_Items
+(
+  type key = indexname;
+  val ord = Term_Ord.fast_indexname_ord;
+);
+
+
 structure Types:
 sig
   include TERM_ITEMS
diff -r 74647c464cbd -r 1c2be1fca2bd src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Oct 25 13:43:12 2024 +0200
+++ b/src/Pure/type_infer.ML	Fri Oct 25 15:39:27 2024 +0200
@@ -65,7 +65,7 @@
 fun add_parms tye T =
   (case deref tye T of
     Type (_, Ts) => fold (add_parms tye) Ts
-  | TVar (xi, _) => if is_param xi then insert (op =) xi else I
+  | TVar (xi, _) => if is_param xi then Indexnames.add_set xi else I
   | _ => I);
 
 fun add_names tye T =
@@ -81,9 +81,9 @@
   let
     val used =
       (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
-    val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
-    val names = Name.invent used ("?" ^ Name.aT) (length parms);
-    val tab = Vartab.make (parms ~~ names);
+    val parms = (fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts Indexnames.empty);
+    val names = Name.invent used ("?" ^ Name.aT) (Indexnames.size parms);
+    val tab = Vartab.make (Indexnames.list_set parms ~~ names);
 
     fun finish_typ T =
       (case deref tye T of