# HG changeset patch
# User wenzelm
# Date 1703590653 -3600
# Node ID b191339a014c4fa58dd3b6c5619f2f4612007201
# Parent  bb07298c5fb03b2f4720368e73a8a96975dc179b
clarified signature;

diff -r bb07298c5fb0 -r b191339a014c src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Dec 26 12:03:54 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Tue Dec 26 12:37:33 2023 +0100
@@ -296,11 +296,10 @@
 
 local
 
-fun name_thm1 (name, pos) =
-  Global_Theory.name_thm Global_Theory.official1 (Thm_Name.flatten name, pos);
+fun name_thms name = split_list #>> burrow (Thm_Name.make_list name) #> op ~~;
 
-fun name_thm2 (name, pos) =
-  Global_Theory.name_thm Global_Theory.unofficial2 (Thm_Name.flatten name, pos);
+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;
 
 fun thm_def (name, pos) thm lthy =
   if #1 name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
@@ -360,10 +359,6 @@
 
   in ((local_thm, global_thm), lthy') end;
 
-fun name_thms (name, pos) =
-  let val thm_names = Thm_Name.make_list name #> map (apfst (rpair pos))
-  in split_list #>> burrow thm_names #> op ~~ end;
-
 in
 
 fun notes target_notes kind facts lthy =
diff -r bb07298c5fb0 -r b191339a014c src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Tue Dec 26 12:03:54 2023 +0100
+++ b/src/Pure/global_theory.ML	Tue Dec 26 12:37:33 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 (uncurry Thm_Name.make_list);
+  |> maps (fn (name, thms) => Thm_Name.make_list (name, Position.none) thms |> map (apfst fst));
 
 
 (* thm_name vs. derivation_id *)
@@ -214,8 +214,7 @@
   let
     val (thms', thy') =
       if name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
-        fold_map (fn (a, th) => Thm.store_zproof (a, pos) th)
-          (Thm_Name.make_list name (Lazy.force thms)) thy
+        fold_map (uncurry Thm.store_zproof) (Thm_Name.make_list (name, pos) (Lazy.force thms)) thy
         |>> Lazy.value
       else (check_thms_lazy thms, thy);
   in (thms', Thm.register_proofs thms' thy') end;
@@ -246,9 +245,9 @@
         |> (name <> "" andalso (post orelse not (Thm.has_name_hint thm))) ?
             Thm.put_name_hint name));
 
-fun name_thms name_flags (name, pos) thms =
-  Thm_Name.make_list name thms
-  |> map (fn (thm_name, thm) => name_thm name_flags (Thm_Name.flatten thm_name, pos) thm);
+fun name_thms name_flags name_pos thms =
+  Thm_Name.make_list name_pos thms
+  |> map (fn (a, thm) => name_thm name_flags (Thm_Name.flatten a) thm);
 
 end;
 
diff -r bb07298c5fb0 -r b191339a014c src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Tue Dec 26 12:03:54 2023 +0100
+++ b/src/Pure/thm_name.ML	Tue Dec 26 12:37:33 2023 +0100
@@ -12,8 +12,8 @@
   type T = string * int
   val ord: T ord
   val print: T -> string
-  val flatten: T -> string
-  val make_list: string -> 'a list -> (T * 'a) list
+  val flatten: T * Position.T -> string * Position.T
+  val make_list: string * Position.T -> 'a list -> ((T * Position.T) * 'a) list
 end;
 
 structure Thm_Name: THM_NAME =
@@ -26,11 +26,11 @@
   if name = "" orelse index = 0 then name
   else name ^ enclose "(" ")" (string_of_int index);
 
-fun flatten (name, index) =
-  if name = "" orelse index = 0 then name
-  else name ^ "_" ^ string_of_int index;
+fun flatten ((name, index), pos) =
+  if name = "" orelse index = 0 then (name, pos)
+  else (name ^ "_" ^ string_of_int index, pos);
 
-fun make_list name [thm] = [((name, 0), thm)]
-  | make_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms;
+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;
 
 end;