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