clarified thm_header command_pos vs. thm_pos;

--- a/src/Doc/Implementation/Logic.thy	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Doc/Implementation/Logic.thy	Fri Jul 19 16:58:52 2024 +0200
@@ -1293,7 +1293,7 @@
   @{define_ML Proofterm.reconstruct_proof:
   "theory -> term -> proof -> proof"} \\
   @{define_ML Proofterm.expand_proof: "theory ->
-  (Proofterm.thm_header -> Thm_Name.T option) -> proof -> proof"} \\
+  (Proofterm.thm_header -> Thm_Name.P option) -> proof -> proof"} \\
   @{define_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
   @{define_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
   @{define_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\

--- a/src/HOL/Tools/inductive_realizer.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -16,7 +16,7 @@
 fun thm_name_of thm =
   (case Proofterm.fold_proof_atoms false (fn PThm ({thm_name, ...}, _) => cons thm_name | _ => I)
       [Thm.proof_of thm] [] of
-    [thm_name] => thm_name
+    [(thm_name, _)] => thm_name
   | _ => raise THM ("thm_name_of: bad proof of theorem", 0, [thm]));
 
 val short_name_of = Thm_Name.short o thm_name_of;

--- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -305,9 +305,9 @@
 
 (** Replace congruence rules by substitution rules **)
 
-fun strip_cong ps (PThm ({thm_name = ("HOL.cong", 0), ...}, _) % _ % _ % SOME x % SOME y %%
+fun strip_cong ps (PThm ({thm_name = (("HOL.cong", 0), _), ...}, _) % _ % _ % SOME x % SOME y %%
       prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
-  | strip_cong ps (PThm ({thm_name = ("HOL.refl", 0), ...}, _) % SOME f %% _) = SOME (f, ps)
+  | strip_cong ps (PThm ({thm_name = (("HOL.refl", 0), _), ...}, _) % SOME f %% _) = SOME (f, ps)
   | strip_cong _ _ = NONE;
 
 val subst_prf = Proofterm.any_head_of (Thm.proof_of @{thm subst});
@@ -330,15 +330,15 @@
 
 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
 
-fun elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD1", 0), _), ...}, _) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
-  | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % P % _ %% prf) =
+  | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD1", 0), _), ...}, _) % P % _ %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
         (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
-  | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
+  | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD2", 0), _), ...}, _) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 [] o
         apsnd (map (make_sym Ts))) (strip_cong [] prf1)
-  | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % P %% prf) =
+  | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD2", 0), _), ...}, _) % _ % P %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
         apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
   | elim_cong_aux _ _ = NONE;

--- a/src/Pure/Build/export_theory.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/Build/export_theory.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -283,8 +283,8 @@
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
     fun expand_name thm_id (header: Proofterm.thm_header) =
-      if #serial header = #serial thm_id then Thm_Name.empty
-      else the_default Thm_Name.empty (lookup_thm_id (Proofterm.thm_header_id header));
+      if #serial header = #serial thm_id then Thm_Name.none
+      else the_default Thm_Name.none (lookup_thm_id (Proofterm.thm_header_id header));
 
     fun entity_markup_thm (serial, (name, i)) =
       let
@@ -314,7 +314,7 @@
           in triple encode_prop (list Thm_Name.encode) encode_proof end
       end;
 
-    fun export_thm (thm_id, thm_name) =
+    fun export_thm (thm_id, (thm_name, _)) =
       let
         val markup = entity_markup_thm (#serial thm_id, thm_name);
         val body =

--- a/src/Pure/Proof/extraction.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -511,9 +511,9 @@
     val procs = maps (rev o fst o snd) types;
     val rtypes = map fst types;
     val typroc = typeof_proc [];
-    fun expand_name ({thm_name, ...}: Proofterm.thm_header) =
+    fun expand_name ({thm_name = (thm_name, _), ...}: Proofterm.thm_header) =
       if Thm_Name.is_empty thm_name orelse member (op =) expand thm_name
-      then SOME Thm_Name.empty else NONE;
+      then SOME Thm_Name.none else NONE;
     val prep = the_default (K I) prep thy' o
       Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
       Proofterm.expand_proof thy' expand_name;
@@ -623,7 +623,7 @@
 
       | corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
           let
-            val {pos, theory_name, thm_name, prop, ...} = thm_header;
+            val {command_pos, theory_name, thm_name = (thm_name, thm_pos), prop, ...} = thm_header;
             val prf = Proofterm.thm_body_proof_open thm_body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val shyps = mk_shyps tye;
@@ -650,8 +650,8 @@
                     val corr_prf = mkabsp shyps corr_prf0;
                     val corr_prop = Proofterm.prop_of corr_prf;
                     val corr_header =
-                      Proofterm.thm_header (serial ()) pos theory_name
-                        (corr_name thm_name vs', 0) corr_prop
+                      Proofterm.thm_header (serial ()) command_pos theory_name
+                        ((corr_name thm_name vs', 0), thm_pos) corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
                     val corr_prf' =
                       Proofterm.proof_combP
@@ -727,7 +727,7 @@
 
       | extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
           let
-            val {pos, theory_name, thm_name, prop, ...} = thm_header;
+            val {command_pos, theory_name, thm_name = (thm_name, thm_pos), prop, ...} = thm_header;
             val prf = Proofterm.thm_body_proof_open thm_body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val shyps = mk_shyps tye;
@@ -772,8 +772,8 @@
                              SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
                     val corr_prop = Proofterm.prop_of corr_prf';
                     val corr_header =
-                      Proofterm.thm_header (serial ()) pos theory_name
-                        (corr_name thm_name vs', 0) corr_prop
+                      Proofterm.thm_header (serial ()) command_pos theory_name
+                        ((corr_name thm_name vs', 0), thm_pos) corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
                     val corr_prf'' =
                       Proofterm.proof_combP (Proofterm.proof_combt

--- a/src/Pure/Proof/proof_checker.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -88,7 +88,7 @@
               (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
           end;
 
-        fun thm_of _ _ (PThm ({thm_name, prop = prop', types = SOME Ts, ...}, _)) =
+        fun thm_of _ _ (PThm ({thm_name = (thm_name, thm_pos), prop = prop', types = SOME Ts, ...}, _)) =
               let
                 val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup thm_name));
                 val prop = Thm.prop_of thm;
@@ -96,9 +96,9 @@
                   if is_equal prop prop' then ()
                   else
                     error ("Duplicate use of theorem name " ^
-                      quote (Global_Theory.print_thm_name thy thm_name) ^ "\n" ^
-                      Syntax.string_of_term_global thy prop ^ "\n\n" ^
-                      Syntax.string_of_term_global thy prop');
+                      quote (Global_Theory.print_thm_name thy thm_name) ^ Position.here thm_pos
+                      ^ "\n" ^ Syntax.string_of_term_global thy prop
+                      ^ "\n\n" ^ Syntax.string_of_term_global thy prop');
               in thm_of_atom thm Ts end
 
           | thm_of _ _ (PAxm (name, _, SOME Ts)) =

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -39,12 +39,12 @@
     val equal_elim_axm = ax Proofterm.equal_elim_axm [];
     val symmetric_axm = ax Proofterm.symmetric_axm [propT];
 
-    fun rew' (PThm ({thm_name = ("Pure.protectD", 0), ...}, _) % _ %%
-        (PThm ({thm_name = ("Pure.protectI", 0), ...}, _) % _ %% prf)) = SOME prf
-      | rew' (PThm ({thm_name = ("Pure.conjunctionD1", 0), ...}, _) % _ % _ %%
-        (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% prf %% _)) = SOME prf
-      | rew' (PThm ({thm_name = ("Pure.conjunctionD2", 0), ...}, _) % _ % _ %%
-        (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% _ %% prf)) = SOME prf
+    fun rew' (PThm ({thm_name = (("Pure.protectD", 0), _), ...}, _) % _ %%
+        (PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _) % _ %% prf)) = SOME prf
+      | rew' (PThm ({thm_name = (("Pure.conjunctionD1", 0), _), ...}, _) % _ % _ %%
+        (PThm ({thm_name = (("Pure.conjunctionI", 0), _), ...}, _) % _ % _ %% prf %% _)) = SOME prf
+      | rew' (PThm ({thm_name = (("Pure.conjunctionD2", 0), _), ...}, _) % _ % _ %%
+        (PThm ({thm_name = (("Pure.conjunctionI", 0), _), ...}, _) % _ % _ %% _ %% prf)) = SOME prf
       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
         (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
       | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
@@ -54,14 +54,14 @@
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
           _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
-        ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
+        ((tg as PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
 
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
           (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
              _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
-        ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
+        ((tg as PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
 
@@ -245,7 +245,7 @@
       (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
   | insert_refl defs Ts prf =
       (case Proofterm.strip_combt prf of
-        (PThm ({thm_name, prop, types = SOME Ts, ...}, _), ts) =>
+        (PThm ({thm_name = (thm_name, _), prop, types = SOME Ts, ...}, _), ts) =>
           if member (op =) defs thm_name then
             let
               val vs = vars_of prop;
@@ -271,11 +271,11 @@
         let
           val cnames = map (fst o dest_Const o fst) defs';
           val expand = Proofterm.fold_proof_atoms true
-            (fn PThm ({serial, thm_name, prop, ...}, _) =>
+            (fn PThm ({serial, thm_name = (thm_name, _), prop, ...}, _) =>
                 if member (op =) defnames thm_name orelse
                   not (exists_Const (member (op =) cnames o #1) prop)
                 then I
-                else Inttab.update (serial, Thm_Name.empty)
+                else Inttab.update (serial, Thm_Name.none)
               | _ => I) [prf] Inttab.empty;
         in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end
       else prf;

--- a/src/Pure/Proof/proof_syntax.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -16,7 +16,7 @@
   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
   val pretty_proof_boxes_of: Proof.context ->
     {full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T
-  val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.T option} ->
+  val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.P option} ->
     thm -> Proofterm.proof
   val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
@@ -104,7 +104,7 @@
   let val U = Term.itselfT T --> propT
   in Const ("Pure.PClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
 
-fun term_of _ (PThm ({serial = i, thm_name = a, types = Ts, ...}, _)) =
+fun term_of _ (PThm ({serial = i, thm_name = (a, _), types = Ts, ...}, _)) =
       fold AppT (these Ts)
         (Const
           (Long_Name.append "thm"
@@ -227,7 +227,7 @@
 fun proof_syntax prf =
   let
     val thm_names = Symset.dest (Proofterm.fold_proof_atoms true
-      (fn PThm ({thm_name, ...}, _) =>
+      (fn PThm ({thm_name = (thm_name, _), ...}, _) =>
           if Thm_Name.is_empty thm_name then I else Symset.insert (Thm_Name.short thm_name)
         | _ => I) [prf] Symset.empty);
     val axm_names = Symset.dest (Proofterm.fold_proof_atoms true
@@ -264,7 +264,7 @@
        excluded = is_some o Global_Theory.lookup_thm_id thy}
   in
     Proofterm.proof_boxes selection [Thm.proof_of thm]
-    |> map (fn ({serial = i, pos, prop, ...}, proof) =>
+    |> map (fn ({serial = i, command_pos, prop, thm_name = (_, thm_pos), ...}, proof) =>
         let
           val proof' = proof
             |> Proofterm.reconstruct_proof thy prop
@@ -276,7 +276,7 @@
           val name = Long_Name.append "thm" (string_of_int i);
         in
           Pretty.item
-           [Pretty.str (name ^ Position.here_list pos ^ ":"), Pretty.brk 1,
+           [Pretty.str (name ^ Position.here_list [command_pos, thm_pos] ^ ":"), Pretty.brk 1,
             Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof']
         end)
     |> Pretty.chunks

--- a/src/Pure/global_theory.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/global_theory.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -13,13 +13,13 @@
   val defined_fact: theory -> string -> bool
   val alias_fact: binding -> string -> theory -> theory
   val hide_fact: bool -> string -> theory -> theory
-  val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
+  val dest_thms: bool -> theory list -> theory -> (Thm_Name.P * thm) list
   val pretty_thm_name: theory -> Thm_Name.T -> Pretty.T
   val print_thm_name: theory -> Thm_Name.T -> string
-  val get_thm_names: theory -> Thm_Name.T Inttab.table
-  val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.T) list
-  val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
-  val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) option
+  val get_thm_names: theory -> Thm_Name.P Inttab.table
+  val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.P) list
+  val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.P option
+  val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.P) option
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
   val transfer_theories: theory -> thm -> thm
@@ -63,7 +63,7 @@
 
 structure Data = Theory_Data
 (
-  type T = Facts.T * Thm_Name.T Inttab.table lazy option;
+  type T = Facts.T * Thm_Name.P Inttab.table lazy option;
   val empty: T = (Facts.empty, NONE);
   fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), NONE);
 );
@@ -86,7 +86,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.list (name, Position.none) thms |> map (apfst fst));
+  |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms);
 
 fun pretty_thm_name thy = Facts.pretty_thm_name (Context.Theory thy) (facts_of thy);
 val print_thm_name = Pretty.string_of oo pretty_thm_name;
@@ -99,7 +99,7 @@
 
 fun make_thm_names thy =
   (dest_thms true (Theory.parents_of thy) thy, Inttab.empty)
-  |-> fold (fn (thm_name, thm) => fn thm_names =>
+  |-> fold (fn ((thm_name, thm_pos), thm) => fn thm_names =>
     (case Thm.derivation_id (Thm.transfer thy thm) of
       NONE => thm_names
     | SOME {serial, theory_name} =>
@@ -107,11 +107,11 @@
           raise THM ("Bad theory name for derivation", 0, [thm])
         else
           (case Inttab.lookup thm_names serial of
-            SOME thm_name' =>
+            SOME (thm_name', thm_pos') =>
               raise THM ("Duplicate use of derivation identity for " ^
-                print_thm_name thy thm_name ^ " vs. " ^
-                print_thm_name thy thm_name', 0, [thm])
-          | NONE => Inttab.update (serial, thm_name) thm_names)));
+                print_thm_name thy thm_name ^ Position.here thm_pos ^ " vs. " ^
+                print_thm_name thy thm_name' ^ Position.here thm_pos', 0, [thm])
+          | NONE => Inttab.update (serial, (thm_name, thm_pos)) thm_names)));
 
 fun lazy_thm_names thy =
   (case thm_names_of thy of
@@ -256,7 +256,7 @@
       No_Name_Flags => thm
     | Name_Flags {post, official} =>
         thm
-        |> (official andalso (post orelse Thm_Name.is_empty (Thm.raw_derivation_name thm))) ?
+        |> (official andalso (post orelse Thm_Name.is_empty (#1 (Thm.raw_derivation_name thm)))) ?
             Thm.name_derivation (name, pos)
         |> (not (Thm_Name.is_empty name) andalso (post orelse not (Thm.has_name_hint thm))) ?
             Thm.put_name_hint name));

--- a/src/Pure/proofterm.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/proofterm.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -9,7 +9,7 @@
 signature PROOFTERM =
 sig
   type thm_header =
-    {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
+    {serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P,
       prop: term, types: typ list option}
   type thm_body
   type thm_node
@@ -38,7 +38,7 @@
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val map_proof_of: (proof -> proof) -> proof_body -> proof_body
-  val thm_header: serial -> Position.T list -> string -> Thm_Name.T -> term -> typ list option ->
+  val thm_header: serial -> Position.T -> string -> Thm_Name.P -> term -> typ list option ->
     thm_header
   val thm_body: proof_body -> thm_body
   val thm_body_proof_raw: thm_body -> proof
@@ -171,8 +171,8 @@
   val reconstruct_proof: theory -> term -> proof -> proof
   val prop_of': term list -> proof -> term
   val prop_of: proof -> term
-  val expand_name_empty: thm_header -> Thm_Name.T option
-  val expand_proof: theory -> (thm_header -> Thm_Name.T option) -> proof -> proof
+  val expand_name_empty: thm_header -> Thm_Name.P option
+  val expand_proof: theory -> (thm_header -> Thm_Name.P option) -> proof -> proof
 
   val standard_vars: Name.context -> term * proof option -> term * proof option
   val standard_vars_term: Name.context -> term -> term
@@ -189,8 +189,8 @@
   val unconstrain_thm_proof: theory -> sorts_proof -> sort list ->
     term -> (serial * proof_body future) list -> proof_body -> term * proof_body
   val get_identity: sort list -> term list -> term -> proof ->
-    {serial: serial, theory_name: string, thm_name: Thm_Name.T} option
-  val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.T
+    {serial: serial, theory_name: string, thm_name: Thm_Name.P} option
+  val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.P
   type thm_id = {serial: serial, theory_name: string}
   val make_thm_id: serial * string -> thm_id
   val thm_header_id: thm_header -> thm_id
@@ -207,7 +207,7 @@
 (** datatype proof **)
 
 type thm_header =
-  {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
+  {serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P,
     prop: term, types: typ list option};
 
 datatype proof =
@@ -254,8 +254,8 @@
 fun no_proof (PBody {oracles, thms, zboxes, zproof, ...}) =
   PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = MinProof};
 
-fun thm_header serial pos theory_name thm_name prop types : thm_header =
-  {serial = serial, pos = pos, theory_name = theory_name, thm_name = thm_name,
+fun thm_header serial command_pos theory_name thm_name prop types : thm_header =
+  {serial = serial, command_pos = command_pos, theory_name = theory_name, thm_name = thm_name,
     prop = prop, types = types};
 
 fun thm_body body = Thm_Body {open_proof = I, body = Future.value body};
@@ -291,7 +291,9 @@
 
 val no_export = Lazy.value ();
 
-fun make_thm ({serial, theory_name, thm_name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
+fun make_thm
+    ({serial, theory_name, thm_name = (thm_name, _), prop, ...}: thm_header)
+    (Thm_Body {body, ...}) =
   (serial, make_thm_node theory_name thm_name prop body no_export);
 
 
@@ -343,8 +345,8 @@
   | no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
   | no_thm_names (prf % t) = no_thm_names prf % t
   | no_thm_names (prf1 %% prf2) = no_thm_names prf1 %% no_thm_names prf2
-  | no_thm_names (PThm ({serial, pos, theory_name, thm_name = _, prop, types}, thm_body)) =
-      PThm (thm_header serial pos theory_name Thm_Name.empty prop types, thm_body)
+  | no_thm_names (PThm ({serial, command_pos, theory_name, thm_name = _, prop, types}, thm_body)) =
+      PThm (thm_header serial command_pos theory_name Thm_Name.none prop types, thm_body)
   | no_thm_names a = a;
 
 fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
@@ -393,10 +395,9 @@
       | zproof (PAxm (a, prop, SOME Ts)) = zproof_const (ZAxiom a) prop Ts
       | zproof (PClass (T, c)) = OFCLASSp (ztyp T, c)
       | zproof (Oracle (a, prop, SOME Ts)) = zproof_const (ZOracle a) prop Ts
-      | zproof (PThm ({serial, pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
-          let
-            val name = (thm_name, try hd pos |> the_default Position.none);
-            val proof_name = ZThm {theory_name = theory_name, thm_name = name, serial = serial};
+      | zproof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
+          let val proof_name =
+            ZThm {theory_name = theory_name, thm_name = thm_name, serial = serial};
           in zproof_const proof_name prop Ts end;
   in zproof end;
 
@@ -421,11 +422,13 @@
   fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
   fn PClass (a, b) => ([b], typ a),
   fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
-  fn PThm ({serial, pos, theory_name, thm_name, prop, types}, Thm_Body {open_proof, body, ...}) =>
-    ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)],
-      pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
-        (map Position.properties_of pos,
-          (prop, (types, map_proof_of open_proof (Future.join body)))))]
+  fn PThm ({serial, command_pos, theory_name, thm_name, prop, types}, Thm_Body {open_proof, body, ...}) =>
+      ([int_atom serial, theory_name],
+        pair (properties o Position.properties_of)
+          (pair Thm_Name.encode_pos
+            (pair (term consts)
+              (pair (option (list typ)) (proof_body consts))))
+        (command_pos, (thm_name, (prop, (types, map_proof_of open_proof (Future.join body))))))]
 and proof_body consts (PBody {oracles, thms, zboxes = _, zproof = _, proof = prf}) =
   triple (list (pair (pair string (properties o Position.properties_of))
       (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
@@ -459,12 +462,14 @@
   fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end,
   fn ([b], a) => PClass (typ a, b),
   fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end,
-  fn ([a, b, c, d], e) =>
+  fn ([ser, theory_name], b) =>
     let
-      val ((x, (y, (z, w)))) =
-        pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) e;
-      val header = thm_header (int_atom a) (map Position.of_properties x) b (c, int_atom d) y z;
-    in PThm (header, thm_body w) end]
+      val ((command_pos, (thm_name, (prop, (types, body))))) =
+        pair (Position.of_properties o properties)
+          (pair Thm_Name.decode_pos
+            (pair (term consts) (pair (option (list typ)) (proof_body consts)))) b;
+      val header = thm_header (int_atom ser) command_pos theory_name thm_name prop types;
+    in PThm (header, thm_body body) end]
 and proof_body consts x =
   let
     val (a, b, c) =
@@ -568,8 +573,8 @@
       | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
       | proof (PClass C) = ofclass C
       | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
-      | proof (PThm ({serial, pos, theory_name, thm_name, prop, types = SOME Ts}, thm_body)) =
-          PThm (thm_header serial pos theory_name thm_name prop (SOME (typs Ts)), thm_body)
+      | proof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts}, thm_body)) =
+          PThm (thm_header serial command_pos theory_name thm_name prop (SOME (typs Ts)), thm_body)
       | proof _ = raise Same.SAME;
   in proof end;
 
@@ -609,8 +614,8 @@
 fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
   | change_types (SOME [T]) (PClass (_, c)) = PClass (T, c)
   | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
-  | change_types types (PThm ({serial, pos, theory_name, thm_name, prop, types = _}, thm_body)) =
-      PThm (thm_header serial pos theory_name thm_name prop types, thm_body)
+  | change_types types (PThm ({serial, command_pos, theory_name, thm_name, prop, types = _}, thm_body)) =
+      PThm (thm_header serial command_pos theory_name thm_name prop types, thm_body)
   | change_types _ prf = prf;
 
 
@@ -774,7 +779,7 @@
           PClass (norm_type_same T, c)
       | norm (Oracle (a, prop, Ts)) =
           Oracle (a, prop, Same.map_option norm_types_same Ts)
-      | norm (PThm ({serial = i, pos = p, theory_name, thm_name, prop = t, types = Ts}, thm_body)) =
+      | norm (PThm ({serial = i, command_pos = p, theory_name, thm_name, prop = t, types = Ts}, thm_body)) =
           PThm (thm_header i p theory_name thm_name t
             (Same.map_option norm_types_same Ts), thm_body)
       | norm _ = raise Same.SAME;
@@ -1035,8 +1040,8 @@
       | proof _ _ (PAxm (a, prop, Ts)) = PAxm (a, prop, typs Ts)
       | proof _ _ (PClass (T, c)) = PClass (typ T, c)
       | proof _ _ (Oracle (a, prop, Ts)) = Oracle (a, prop, typs Ts)
-      | proof _ _ (PThm ({serial, pos, theory_name, thm_name, prop, types}, thm_body)) =
-          PThm (thm_header serial pos theory_name thm_name prop (typs types), thm_body)
+      | proof _ _ (PThm ({serial, command_pos, theory_name, thm_name, prop, types}, thm_body)) =
+          PThm (thm_header serial command_pos theory_name thm_name prop (typs types), thm_body)
       | proof _ _ _ = raise Same.SAME;
 
     val k = length prems;
@@ -1458,7 +1463,7 @@
       | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
       | subst _ _ (PClass (T, c)) = PClass (substT T, c)
       | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
-      | subst _ _ (PThm ({serial = i, pos = p, theory_name, thm_name, prop, types}, thm_body)) =
+      | subst _ _ (PThm ({serial = i, command_pos = p, theory_name, thm_name, prop, types}, thm_body)) =
           PThm (thm_header i p theory_name thm_name prop (Same.map_option substTs types), thm_body)
       | subst _ _ _ = raise Same.SAME;
   in fn t => subst 0 0 t handle Same.SAME => t end;
@@ -1633,7 +1638,7 @@
   | guess_name (prf %% PClass _) = guess_name prf
   | guess_name (prf % NONE) = guess_name prf
   | guess_name (prf % SOME (Var _)) = guess_name prf
-  | guess_name _ = Thm_Name.empty;
+  | guess_name _ = Thm_Name.none;
 
 
 (* generate constraints for proof term *)
@@ -1745,7 +1750,8 @@
               | SOME Ts => (Ts, env));
             val prop' = subst_atomic_types (prop_types ~~ Ts)
               (forall_intr_variables_term prop) handle ListPair.UnequalLengths =>
-                error ("Wrong number of type arguments for " ^ quote (Thm_Name.print (guess_name prf)))
+                error ("Wrong number of type arguments for " ^
+                  quote (Thm_Name.print_pos (guess_name prf)))
           in (prop', change_types (SOME Ts) prf, [], env', vTs) end;
 
     fun head_norm (prop, prf, cnstrts, env, vTs) =
@@ -1933,7 +1939,7 @@
 (* expand and reconstruct subproofs *)
 
 fun expand_name_empty (header: thm_header) =
-  if Thm_Name.is_empty (#thm_name header) then SOME Thm_Name.empty else NONE;
+  if Thm_Name.is_empty (#1 (#thm_name header)) then SOME Thm_Name.none else NONE;
 
 fun expand_proof thy expand_name prf =
   let
@@ -1952,10 +1958,10 @@
           let val (seen', maxidx', prf') = expand seen maxidx prf
           in (seen', maxidx', prf' % t) end
       | expand seen maxidx (prf as PThm (header, thm_body)) =
-          let val {serial, pos, theory_name, thm_name, prop, types} = header in
+          let val {serial, command_pos, theory_name, thm_name, prop, types} = header in
             (case expand_name header of
               SOME thm_name' =>
-                if #1 thm_name' = "" andalso is_some types then
+                if #1 (#1 thm_name') = "" andalso is_some types then
                   let
                     val (seen', maxidx', prf') =
                       (case Inttab.lookup seen serial of
@@ -1974,7 +1980,7 @@
                   in (seen', maxidx' + maxidx + 1, prf'') end
                 else if thm_name' <> thm_name then
                   (seen, maxidx,
-                    PThm (thm_header serial pos theory_name thm_name' prop types, thm_body))
+                    PThm (thm_header serial command_pos theory_name thm_name' prop types, thm_body))
                 else (seen, maxidx, prf)
             | NONE => (seen, maxidx, prf))
           end
@@ -2216,7 +2222,7 @@
       if export_enabled () then new_prf ()
       else
         (case strip_combt (proof_head_of proof0) of
-          (PThm ({serial = ser, thm_name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
+          (PThm ({serial = ser, thm_name = (a, _), prop = prop', types = NONE, ...}, thm_body'), args') =>
             if (#1 a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
               let
                 val Thm_Body {body = body', ...} = thm_body';
@@ -2249,7 +2255,7 @@
     val theory_name = Context.theory_long_name thy;
     val thm = (i, make_thm_node theory_name name prop1 thm_body export);
 
-    val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE;
+    val header = thm_header i (Position.thread_data ()) theory_name (name, pos) prop1 NONE;
     val head = PThm (header, Thm_Body {open_proof = open_proof, body = thm_body});
     val argst =
       if unconstrain then
@@ -2288,7 +2294,7 @@
   end;
 
 fun get_approximative_name shyps hyps prop prf =
-  Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.empty;
+  Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.none;
 
 
 (* thm_id *)
@@ -2307,7 +2313,7 @@
 fun get_id shyps hyps prop prf : thm_id option =
   (case get_identity shyps hyps prop prf of
     NONE => NONE
-  | SOME {serial, theory_name, thm_name, ...} =>
+  | SOME {serial, theory_name, thm_name = (thm_name, _), ...} =>
       if Thm_Name.is_empty thm_name then NONE else SOME (make_thm_id (serial, theory_name)));
 
 fun this_id NONE _ = false

--- a/src/Pure/thm.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/thm.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -120,8 +120,8 @@
   val derivation_closed: thm -> bool
   val derivation_name: thm -> Thm_Name.T
   val derivation_id: thm -> Proofterm.thm_id option
-  val raw_derivation_name: thm -> Thm_Name.T
-  val expand_name: thm -> Proofterm.thm_header -> Thm_Name.T option
+  val raw_derivation_name: thm -> Thm_Name.P
+  val expand_name: thm -> Proofterm.thm_header -> Thm_Name.P option
   val name_derivation: Thm_Name.P -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
@@ -1131,13 +1131,13 @@
         NONE => K false
       | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header);
     fun expand header =
-      if self_id header orelse Thm_Name.is_empty (#thm_name header)
-      then SOME Thm_Name.empty else NONE;
+      if self_id header orelse Thm_Name.is_empty (#1 (#thm_name header))
+      then SOME Thm_Name.none else NONE;
   in expand end;
 
 (*deterministic name of finished proof*)
 fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
-  Proofterm.get_approximative_name shyps hyps prop (proof_of thm);
+  #1 (Proofterm.get_approximative_name shyps hyps prop (proof_of thm));
 
 (*identified PThm node*)
 fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =

--- a/src/Pure/thm_deps.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/thm_deps.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -59,7 +59,7 @@
       else
         let val thm_id = Proofterm.thm_id (i, thm_node) in
           (case lookup thm_id of
-            SOME thm_name =>
+            SOME (thm_name, _) =>
               Inttab.update (i, SOME (thm_id, thm_name)) res
           | NONE =>
               Inttab.update (i, NONE) res

--- a/src/Pure/thm_name.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/thm_name.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -26,9 +26,12 @@
   val print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string
   val print_suffix: T -> string
   val print: T -> string
+  val print_pos: P -> string
   val short: T -> string
   val encode: T XML.Encode.T
   val decode: T XML.Decode.T
+  val encode_pos: P XML.Encode.T
+  val decode_pos: P XML.Decode.T
 end;
 
 structure Thm_Name: THM_NAME =
@@ -106,6 +109,8 @@
 
 fun print (name, index) = name ^ print_suffix (name, index);
 
+fun print_pos (thm_name, pos) = print thm_name ^ Position.here pos;
+
 fun short (name, index) =
   if name = "" orelse index = 0 then name
   else name ^ "_" ^ string_of_int index;
@@ -116,4 +121,7 @@
 val encode = let open XML.Encode in pair string int end;
 val decode = let open XML.Decode in pair string int end;
 
+val encode_pos = let open XML.Encode in pair encode (properties o Position.properties_of) end;
+val decode_pos = let open XML.Decode in pair decode (Position.of_properties o properties) end;
+
 end;