clarified signature;

--- a/src/Pure/Isar/generic_target.ML	Wed Dec 27 15:34:47 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Wed Dec 27 15:50:17 2023 +0100
@@ -296,7 +296,7 @@
 
 local
 
-fun name_thms name = split_list #>> burrow (Thm_Name.make_list name) #> op ~~;
+fun name_thms name = split_list #>> burrow (Thm_Name.list name) #> op ~~;
 
 val name_thm1 = Global_Theory.name_thm Global_Theory.official1 o Thm_Name.flatten;
 val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2 o Thm_Name.flatten;

--- a/src/Pure/global_theory.ML	Wed Dec 27 15:34:47 2023 +0100
+++ b/src/Pure/global_theory.ML	Wed Dec 27 15:50:17 2023 +0100
@@ -83,7 +83,7 @@
 
 fun dest_thms verbose prev_thys thy =
   Facts.dest_static verbose (map facts_of prev_thys) (facts_of thy)
-  |> maps (fn (name, thms) => Thm_Name.make_list (name, Position.none) thms |> map (apfst fst));
+  |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms |> map (apfst fst));
 
 
 (* thm_name vs. derivation_id *)
@@ -215,7 +215,7 @@
 
 fun store_proofs_lazy zproof name thms thy =
   if zproof_enabled zproof (#1 name) then
-    fold_map (uncurry Thm.store_zproof) (Thm_Name.make_list name (Lazy.force thms)) thy
+    fold_map (uncurry Thm.store_zproof) (Thm_Name.list name (Lazy.force thms)) thy
     |>> Lazy.value
   else (check_thms_lazy thms, thy);
 
@@ -250,7 +250,7 @@
             Thm.put_name_hint name));
 
 fun name_thms name_flags name_pos thms =
-  Thm_Name.make_list name_pos thms
+  Thm_Name.list name_pos thms
   |> map (fn (a, thm) => name_thm name_flags (Thm_Name.flatten a) thm);
 
 end;
@@ -261,7 +261,7 @@
 fun add_facts (b, fact) thy =
   let
     val check =
-      Thm_Name.make_list (Sign.full_name_pos thy b) #> map (fn ((name, pos), thm) =>
+      Thm_Name.list (Sign.full_name_pos thy b) #> map (fn ((name, pos), thm) =>
         let
           fun err msg =
             error ("Malformed global fact " ^

--- a/src/Pure/thm_name.ML	Wed Dec 27 15:34:47 2023 +0100
+++ b/src/Pure/thm_name.ML	Wed Dec 27 15:50:17 2023 +0100
@@ -13,7 +13,7 @@
   val ord: T ord
   val print: T -> string
   val flatten: T * Position.T -> string * Position.T
-  val make_list: string * Position.T -> 'a list -> ((T * Position.T) * 'a) list
+  val list: string * Position.T -> 'a list -> ((T * Position.T) * 'a) list
 end;
 
 structure Thm_Name: THM_NAME =
@@ -30,7 +30,7 @@
   if name = "" orelse index = 0 then (name, pos)
   else (name ^ "_" ^ string_of_int index, pos);
 
-fun make_list (name, pos) [thm] = [(((name, 0), pos), thm)]
-  | make_list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms;
+fun list (name, pos: Position.T) [thm] = [(((name, 0): T, pos), thm)]
+  | list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms;
 
 end;