# HG changeset patch
# User wenzelm
# Date 1703588634 -3600
# Node ID bb07298c5fb03b2f4720368e73a8a96975dc179b
# Parent  e9828380e7e3c24bce241ac44e8eead20fef70e5
proper Thm_Name.make_list for thm_definition;
tuned modules;

diff -r e9828380e7e3 -r bb07298c5fb0 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Dec 24 20:35:22 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Tue Dec 26 12:03:54 2023 +0100
@@ -296,12 +296,18 @@
 
 local
 
+fun name_thm1 (name, pos) =
+  Global_Theory.name_thm Global_Theory.official1 (Thm_Name.flatten name, pos);
+
+fun name_thm2 (name, pos) =
+  Global_Theory.name_thm Global_Theory.unofficial2 (Thm_Name.flatten name, pos);
+
 fun thm_def (name, pos) thm lthy =
-  if name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
-    Local_Theory.background_theory_result (Thm.store_zproof ((name, 0), pos) thm) lthy  (* FIXME proper Thm_Name.T *)
+  if #1 name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
+    Local_Theory.background_theory_result (Thm.store_zproof (name, pos) thm) lthy
   else (thm, lthy);
 
-fun thm_definition (name, thm0) lthy =
+fun thm_definition (name_pos, thm0) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
 
@@ -323,8 +329,7 @@
       |> Drule.zero_var_indexes_list;
 
     (*thm definition*)
-    val (global_thm, lthy') =
-      thm_def name (Global_Theory.name_thm Global_Theory.official1 name schematic_thm) lthy;
+    val (global_thm, lthy') = thm_def name_pos (name_thm1 name_pos schematic_thm) lthy;
 
     (*import fixes*)
     val (tvars, vars) =
@@ -351,11 +356,13 @@
         handle THM _ => raise THM ("Failed to re-import result", 0, fixed_thm :: asms'))
       |> Local_Defs.contract lthy defs (Thm.cprop_of thm)
       |> Goal.norm_result lthy
-      |> Global_Theory.name_thm Global_Theory.unofficial2 name;
+      |> name_thm2 name_pos;
 
   in ((local_thm, global_thm), lthy') end;
 
-fun name_thms name = split_list #>> burrow (Global_Theory.name_multi name) #> op ~~;
+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
 
diff -r e9828380e7e3 -r bb07298c5fb0 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun Dec 24 20:35:22 2023 +0100
+++ b/src/Pure/global_theory.ML	Tue Dec 26 12:03:54 2023 +0100
@@ -25,7 +25,6 @@
   val get_thm_name: theory -> Thm_Name.T * Position.T -> thm
   val register_proofs_lazy: string * Position.T -> thm list lazy -> theory -> thm list lazy * theory
   val register_proofs: string * Position.T -> thm list -> theory -> thm list * theory
-  val name_multi: string * Position.T -> thm list -> ((string * Position.T) * thm) list
   type name_flags
   val unnamed: name_flags
   val official1: name_flags
@@ -227,9 +226,6 @@
 
 (* name theorems *)
 
-fun name_multi (name, pos) =
-  Thm_Name.make_list name #> (map o apfst) (fn thm_name => (Thm_Name.flatten thm_name, pos));
-
 abstype name_flags = No_Name_Flags | Name_Flags of {post: bool, official: bool}
 with
 
@@ -250,8 +246,9 @@
         |> (name <> "" andalso (post orelse not (Thm.has_name_hint thm))) ?
             Thm.put_name_hint name));
 
-fun name_thms name_flags name_pos =
-  name_multi name_pos #> map (uncurry (name_thm name_flags));
+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);
 
 end;