src/Pure/thm_name.ML

--- a/src/Pure/thm_name.ML	Mon Jun 10 14:29:33 2024 +0200
+++ b/src/Pure/thm_name.ML	Mon Jun 10 14:53:54 2024 +0200
@@ -15,6 +15,7 @@
   structure Table: TABLE
   val empty: T
   val is_empty: T -> bool
+  val make_list: string * 'a list -> (T * 'a) list
 
   type P = T * Position.T
   val none: P
@@ -44,6 +45,9 @@
 val empty: T = ("", 0);
 fun is_empty ((a, _): T) = a = "";
 
+fun make_list (a, [b]) = [((a, 0): T, b)]
+  | make_list (a, bs) = map_index (fn (i, b) => ((a, i + 1), b)) bs;
+
 
 (* type P *)