# HG changeset patch
# User wenzelm
# Date 1717797211 -7200
# Node ID 8a9588ffc133657e50f9df7b889a1996fac4f4c2
# Parent  eec06d39e5fab2d41b0ecca3773be010d3582f63
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;

diff -r eec06d39e5fa -r 8a9588ffc133 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Doc/Implementation/Logic.thy	Fri Jun 07 23:53:31 2024 +0200
@@ -1293,7 +1293,7 @@
   @{define_ML Proofterm.reconstruct_proof:
   "theory -> term -> proof -> proof"} \\
   @{define_ML Proofterm.expand_proof: "theory ->
-  (Proofterm.thm_header -> string option) -> proof -> proof"} \\
+  (Proofterm.thm_header -> Thm_Name.T 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"} \\
diff -r eec06d39e5fa -r 8a9588ffc133 src/HOL/Proofs/ex/Proof_Terms.thy
--- a/src/HOL/Proofs/ex/Proof_Terms.thy	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Fri Jun 07 23:53:31 2024 +0200
@@ -35,7 +35,7 @@
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (op =) name) [body] [];
+      (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
 \<close>
 
 text \<open>
diff -r eec06d39e5fa -r 8a9588ffc133 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -187,7 +187,7 @@
       |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0)
       |> Local_Theory.note ((\<^binding>\<open>thms\<close>, []), assm_ths0)
 
-    fun ref_of th = (Facts.named (Thm.derivation_name th), [])
+    fun ref_of th = (Facts.named (Thm_Name.short (Thm.derivation_name th)), [])
     val ref_of_assms = (Facts.named assm_name, [])
   in
     Sledgehammer_Tactics.sledgehammer_as_oracle_tac lthy
diff -r eec06d39e5fa -r 8a9588ffc133 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -224,8 +224,7 @@
       let
         val name = Long_Name.append qualifier base;
         val pos = Position.thread_data ();
-        val thms' =
-          Thm_Name.list (name, pos) thms |> map (uncurry (Thm.name_derivation o Thm_Name.short));
+        val thms' = Thm_Name.list (name, pos) thms |> map (uncurry Thm.name_derivation);
       in (local_name, thms') :: noted end
     else ((local_name, thms) :: name_noted_thms qualifier base noted);
 
diff -r eec06d39e5fa -r 8a9588ffc133 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -305,7 +305,7 @@
         if Inttab.defined seen i then (x, seen)
         else
           let
-            val name = Proofterm.thm_node_name thm_node;
+            val name = Thm_Name.short (Proofterm.thm_node_name thm_node);
             val prop = Proofterm.thm_node_prop thm_node;
             val body = Future.join (Proofterm.thm_node_body thm_node);
             val (x', seen') =
diff -r eec06d39e5fa -r 8a9588ffc133 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -76,7 +76,7 @@
   let
     fun app_thm map_name (_, thm_node) (accum as (num_thms, names)) =
       let
-        val name = Proofterm.thm_node_name thm_node
+        val name = Thm_Name.short (Proofterm.thm_node_name thm_node)
         val body = Proofterm.thm_node_body thm_node
         val (anonymous, enter_class) =
           (* The "name = outer_name" case caters for the uncommon case where the proved theorem
diff -r eec06d39e5fa -r 8a9588ffc133 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -127,7 +127,8 @@
     val (thm', thy') = thy
       |> Sign.root_path
       |> Global_Theory.store_thm
-        (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
+        (Binding.qualified_name
+          (space_implode "_" (Thm_Name.short ind_name :: vs @ ["correctness"])), thm)
       ||> Sign.restore_naming thy;
 
     val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
@@ -201,7 +202,8 @@
     val exh_name = Thm.derivation_name exhaust;
     val (thm', thy') = thy
       |> Sign.root_path
-      |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
+      |> Global_Theory.store_thm
+          (Binding.qualified_name (Thm_Name.short exh_name ^ "_P_correctness"), thm)
       ||> Sign.restore_naming thy;
 
     val P = Var (("P", 0), rT' --> HOLogic.boolT);
diff -r eec06d39e5fa -r 8a9588ffc133 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -13,11 +13,13 @@
 structure InductiveRealizer : INDUCTIVE_REALIZER =
 struct
 
-fun name_of_thm thm =
-  (case Proofterm.fold_proof_atoms false (fn PThm ({name, ...}, _) => cons name | _ => I)
+fun thm_name_of thm =
+  (case Proofterm.fold_proof_atoms false (fn PThm ({thm_name, ...}, _) => cons thm_name | _ => I)
       [Thm.proof_of thm] [] of
-    [name] => name
-  | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
+    [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;
 
 fun prf_of thy =
   Thm.transfer thy #>
@@ -61,7 +63,7 @@
       (Logic.strip_imp_concl (Thm.prop_of (hd intrs))));
     val params = map dest_Var (take nparms ts);
     val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
-    fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
+    fun constr_of_intr intr = (Binding.name (Long_Name.base_name (short_name_of intr)),
       map (Logic.unvarifyT_global o snd)
         (subtract (op =) params (rev (Term.add_vars (Thm.prop_of intr) []))) @
       filter_out (equal Extraction.nullT)
@@ -193,7 +195,7 @@
             then fold_rev (absfree o dest_Free) xs HOLogic.unit
             else fold_rev (absfree o dest_Free) xs
               (list_comb
-                (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
+                (Free ("r" ^ Long_Name.base_name (short_name_of intr),
                   map fastype_of (rev args) ---> conclT), rev args))
           end
 
@@ -216,7 +218,7 @@
       end) (premss ~~ dummies);
     val frees = fold Term.add_frees fs [];
     val Ts = map fastype_of fs;
-    fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr)
+    fun name_of_fn intr = "r" ^ Long_Name.base_name (short_name_of intr)
   in
     fst (fold_map (fn concl => fn names =>
       let val T = Extraction.etype_of thy vs [] concl
@@ -273,7 +275,7 @@
 
 fun add_ind_realizer rsets intrs induct raw_induct elims vs thy =
   let
-    val qualifier = Long_Name.qualifier (name_of_thm induct);
+    val qualifier = Long_Name.qualifier (short_name_of induct);
     val inducts = Global_Theory.get_thms thy (Long_Name.qualify qualifier "inducts");
     val iTs = rev (Term.add_tvars (Thm.prop_of (hd intrs)) []);
     val ar = length vs + length iTs;
@@ -354,11 +356,11 @@
         {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
           no_elim = false, no_ind = false, skip_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
-          ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
+          ((Binding.name (Long_Name.base_name (short_name_of intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
              (rintrs ~~ maps snd rss)) []) ||>
       Sign.root_path;
-    val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
+    val thy3 = fold (Global_Theory.hide_fact false o short_name_of) (#intrs ind_info) thy3';
 
     (** realizer for induction rule **)
 
@@ -413,7 +415,7 @@
               mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
             realizers @ (case realizers of
              [(((ind, corr), rlz), r)] =>
-               [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
+               [mk_realizer thy'' (vs' @ Ps) ((Long_Name.qualify qualifier "induct", 0),
                   ind, corr, rlz, r)]
            | _ => [])) thy''
       end;
@@ -463,10 +465,10 @@
                DEPTH_SOLVE_1 o
                FIRST' [assume_tac ctxt, eresolve_tac ctxt [allE], eresolve_tac ctxt [impE]])) 1)]);
         val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
-          (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
+          (short_name_of elim :: vs @ Ps @ ["correctness"])), thm) thy
       in
         Extraction.add_realizers_i
-          [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
+          [mk_realizer thy' (vs @ Ps) (thm_name_of elim, elim, thm', rlz, r)] thy'
       end;
 
     (** add realizers to theory **)
@@ -474,7 +476,7 @@
     val thy4 = fold add_ind_realizer (subsets Ps) thy3;
     val thy5 = Extraction.add_realizers_i
       (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
-         (name_of_thm rule, rule, rrule, rlz,
+         (thm_name_of rule, rule, rrule, rlz,
             list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (Thm.prop_of rule) []))))))
               (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
     val elimps = map_filter (fn ((s, intrs), p) =>
diff -r eec06d39e5fa -r 8a9588ffc133 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -305,9 +305,9 @@
 
 (** Replace congruence rules by substitution rules **)
 
-fun strip_cong ps (PThm ({name = "HOL.cong", ...}, _) % _ % _ % 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 ({name = "HOL.refl", ...}, _) % 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 ({name = "HOL.iffD1", ...}, _) % _ % _ %% 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 ({name = "HOL.iffD1", ...}, _) % 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 ({name = "HOL.iffD2", ...}, _) % _ % _ %% 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 ({name = "HOL.iffD2", ...}, _) % _ % 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;
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Build/export_theory.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -283,11 +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 ""
-      else
-        (case lookup_thm_id (Proofterm.thm_header_id header) of
-          NONE => ""
-        | SOME thm_name => Thm_Name.print thm_name);
+      if #serial header = #serial thm_id then Thm_Name.empty
+      else the_default Thm_Name.empty (lookup_thm_id (Proofterm.thm_header_id header));
 
     fun entity_markup_thm (serial, (name, i)) =
       let
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -296,8 +296,8 @@
 
 local
 
-val name_thm1 = Global_Theory.name_thm Global_Theory.official1 o Thm_Name.short;
-val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2 o Thm_Name.short;
+val name_thm1 = Global_Theory.name_thm Global_Theory.official1;
+val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2;
 
 fun thm_def (name, pos) thm lthy =
   if #1 name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -11,7 +11,7 @@
   val add_realizes_eqns : string list -> theory -> theory
   val add_typeof_eqns_i : ((term * term) list * (term * term)) list -> theory -> theory
   val add_typeof_eqns : string list -> theory -> theory
-  val add_realizers_i : (string * (string list * term * Proofterm.proof)) list
+  val add_realizers_i : (Thm_Name.T * (string list * term * Proofterm.proof)) list
     -> theory -> theory
   val add_realizers : (thm * (string list * string * string)) list
     -> theory -> theory
@@ -118,8 +118,11 @@
 
 val change_types = Proofterm.change_types o SOME;
 
-fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
-fun corr_name s vs = extr_name s vs ^ "_correctness";
+fun extr_name ((name, i): Thm_Name.T) vs =
+  (Long_Name.append "extr" (space_implode "_" (name :: vs)), i);
+
+fun corr_name thm_name vs =
+  extr_name thm_name vs |>> suffix "_correctness";
 
 fun msg d s = writeln (Symbol.spaces d ^ s);
 
@@ -202,16 +205,16 @@
      typeof_eqns : rules,
      types : (string * ((term -> term option) list *
        (term -> typ -> term -> typ -> term) option)) list,
-     realizers : (string list * (term * proof)) list Symtab.table,
+     realizers : (string list * (term * proof)) list Thm_Name.Table.table,
      defs : thm list,
-     expand : string list,
+     expand : Thm_Name.T list,
      prep : (theory -> proof -> proof) option}
 
   val empty =
     {realizes_eqns = empty_rules,
      typeof_eqns = empty_rules,
      types = [],
-     realizers = Symtab.empty,
+     realizers = Thm_Name.Table.empty,
      defs = [],
      expand = [],
      prep = NONE};
@@ -224,7 +227,7 @@
     {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
      typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
      types = AList.merge (op =) (K true) (types1, types2),
-     realizers = Symtab.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2),
+     realizers = Thm_Name.Table.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2),
      defs = Library.merge Thm.eq_thm (defs1, defs2),
      expand = Library.merge (op =) (expand1, expand2),
      prep = if is_some prep1 then prep1 else prep2};
@@ -319,7 +322,7 @@
   in
     ExtractionData.put
       {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
-       realizers = fold (Symtab.cons_list o prep_rlz thy) rs realizers,
+       realizers = fold (Thm_Name.Table.cons_list o prep_rlz thy) rs realizers,
        defs = defs, expand = expand, prep = prep} thy
   end
 
@@ -335,8 +338,8 @@
     val rd = Proof_Syntax.read_proof thy' true false;
   in fn (thm, (vs, s1, s2)) =>
     let
-      val name = Thm.derivation_name thm;
-      val _ = name <> "" orelse error "add_realizers: unnamed theorem";
+      val thm_name = Thm.derivation_name thm;
+      val _ = if Thm_Name.is_empty thm_name then error "add_realizers: unnamed theorem" else ();
       val prop = Thm.unconstrainT thm |> Thm.prop_of |>
         Pattern.rewrite_term thy' (map (Logic.dest_equals o Thm.prop_of) defs) [];
       val vars = vars_of prop;
@@ -357,7 +360,7 @@
       val r = Logic.list_implies (shyps,
         fold_rev Logic.all (map (get_var_type r') vars) r');
       val prf = Proofterm.reconstruct_proof thy' r (rd s2);
-    in (name, (vs, (t, prf))) end
+    in (thm_name, (vs, (t, prf))) end
   end;
 
 val add_realizers_i = gen_add_realizers
@@ -411,8 +414,8 @@
     val {realizes_eqns, typeof_eqns, types, realizers,
       defs, expand, prep} = ExtractionData.get thy;
 
-    val name = Thm.derivation_name thm;
-    val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
+    val thm_name = Thm.derivation_name thm;
+    val _ = if Thm_Name.is_empty thm_name then error "add_expand_thm: unnamed theorem" else ();
   in
     thy |> ExtractionData.put
       (if is_def then
@@ -425,7 +428,7 @@
       else
         {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
          realizers = realizers, defs = defs,
-         expand = insert (op =) name expand, prep = prep})
+         expand = insert (op =) thm_name expand, prep = prep})
   end;
 
 fun extraction_expand is_def =
@@ -508,8 +511,9 @@
     val procs = maps (rev o fst o snd) types;
     val rtypes = map fst types;
     val typroc = typeof_proc [];
-    fun expand_name ({name, ...}: Proofterm.thm_header) =
-      if name = "" orelse member (op =) expand name then SOME "" else NONE;
+    fun expand_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;
     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;
@@ -539,7 +543,8 @@
         (T, Sign.defaultS thy)) tye;
 
     fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
-    fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
+    fun filter_thm_name (a: Thm_Name.T) =
+      map_filter (fn (b, x) => if a = b then SOME x else NONE);
 
     fun app_rlz_rews Ts vs t =
       strip_abs (length Ts)
@@ -618,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, name, prop, ...} = thm_header;
+            val {pos, theory_name, thm_name, 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;
@@ -629,14 +634,16 @@
               else snd (extr d vs ts Ts hs prf0 defs)
           in
             if T = nullT andalso realizes_null vs' prop aconv prop then (prf0, defs)
-            else (case Symtab.lookup realizers name of
-              NONE => (case find vs' (find' name defs') of
+            else (case Thm_Name.Table.lookup realizers thm_name of
+              NONE => (case find vs' (filter_thm_name thm_name defs') of
                 NONE =>
                   let
                     val _ = T = nullT orelse error "corr: internal error";
-                    val _ = msg d ("Building correctness proof for " ^ quote name ^
-                      (if null vs' then ""
-                       else " (relevant variables: " ^ commas_quote vs' ^ ")"));
+                    val _ =
+                      msg d ("Building correctness proof for " ^
+                        quote (Thm_Name.short thm_name) ^
+                        (if null vs' then ""
+                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
                     val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
                     val (corr_prf0, defs'') = corr (d + 1) vs' [] [] []
                       (rev shyps) NONE prf' prf' defs';
@@ -644,7 +651,7 @@
                     val corr_prop = Proofterm.prop_of corr_prf;
                     val corr_header =
                       Proofterm.thm_header (serial ()) pos theory_name
-                        (corr_name name vs') corr_prop
+                        (corr_name thm_name vs') corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
                     val corr_prf' =
                       Proofterm.proof_combP
@@ -656,15 +663,16 @@
                       mkabsp shyps
                   in
                     (Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs),
-                      (name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'')
+                      (thm_name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'')
                   end
               | SOME (_, (_, prf')) =>
                   (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs'))
             | SOME rs => (case find vs' rs of
                 SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
               | NONE => error ("corr: no realizer for instance of theorem " ^
-                  quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
-                    (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
+                  quote (Thm_Name.short thm_name) ^ ":\n" ^
+                    Syntax.string_of_term_global thy'
+                      (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
           end
 
       | corr d vs ts Ts hs cs _ (prf0 as PAxm (s, prop, SOME Ts')) _ defs =
@@ -674,7 +682,7 @@
           in
             if etype_of thy' vs' [] prop = nullT andalso
               realizes_null vs' prop aconv prop then (prf0, defs)
-            else case find vs' (Symtab.lookup_list realizers s) of
+            else case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of
               SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
                 defs)
             | NONE => error ("corr: no realizer for instance of axiom " ^
@@ -719,19 +727,20 @@
 
       | extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
           let
-            val {pos, theory_name, name = s, prop, ...} = thm_header;
+            val {pos, theory_name, thm_name, 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;
             val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
           in
-            case Symtab.lookup realizers s of
-              NONE => (case find vs' (find' s defs) of
+            case Thm_Name.Table.lookup realizers thm_name of
+              NONE => (case find vs' (filter_thm_name thm_name defs) of
                 NONE =>
                   let
-                    val _ = msg d ("Extracting " ^ quote s ^
-                      (if null vs' then ""
-                       else " (relevant variables: " ^ commas_quote vs' ^ ")"));
+                    val _ =
+                      msg d ("Extracting " ^ quote (Thm_Name.short thm_name) ^
+                        (if null vs' then ""
+                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
                     val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
                     val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs;
                     val (corr_prf, defs'') = corr (d + 1) vs' [] [] []
@@ -743,7 +752,7 @@
                     val args' = filter (fn v => Logic.occs (v, nt)) args;
                     val t' = mkabs args' nt;
                     val T = fastype_of t';
-                    val cname = extr_name s vs';
+                    val cname = Thm_Name.short (extr_name thm_name vs');
                     val c = Const (cname, T);
                     val u = mkabs args (list_comb (c, args'));
                     val eqn = Logic.mk_equals (c, t');
@@ -764,7 +773,7 @@
                     val corr_prop = Proofterm.prop_of corr_prf';
                     val corr_header =
                       Proofterm.thm_header (serial ()) pos theory_name
-                        (corr_name s vs') corr_prop
+                        (corr_name thm_name vs') corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
                     val corr_prf'' =
                       Proofterm.proof_combP (Proofterm.proof_combt
@@ -775,13 +784,14 @@
                       mkabsp shyps
                   in
                     (subst_TVars tye' u,
-                      (s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'')
+                      (thm_name, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'')
                   end
               | SOME ((_, u), _) => (subst_TVars tye' u, defs))
             | SOME rs => (case find vs' rs of
                 SOME (t, _) => (subst_TVars tye' t, defs)
               | NONE => error ("extr: no realizer for instance of theorem " ^
-                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
+                  quote (Thm_Name.short thm_name) ^ ":\n" ^
+                    Syntax.string_of_term_global thy' (Envir.beta_norm
                     (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))
           end
 
@@ -790,7 +800,7 @@
             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
           in
-            case find vs' (Symtab.lookup_list realizers s) of
+            case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of
               SOME (t, _) => (subst_TVars tye' t, defs)
             | NONE => error ("extr: no realizer for instance of axiom " ^
                 quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
@@ -805,26 +815,27 @@
         val prop = Thm.prop_of thm;
         val prf = Thm.proof_of thm;
         val name = Thm.derivation_name thm;
-        val _ = name <> "" orelse error "extraction: unnamed theorem";
+        val _ = if Thm_Name.is_empty name then error "extraction: unnamed theorem" else ();
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
-          quote name ^ " has no computational content")
+          quote (Thm_Name.short name) ^ " has no computational content")
       in Proofterm.reconstruct_proof thy' prop prf end;
 
     val defs =
       fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
         thm_vss [];
 
-    fun add_def (s, (vs, ((t, u)))) thy =
+    fun add_def (name, (vs, ((t, u)))) thy =
       let
         val ft = Type.legacy_freeze t;
         val fu = Type.legacy_freeze u;
         val head = head_of (strip_abs_body fu);
-        val b = Binding.qualified_name (extr_name s vs);
+        val b = Binding.qualified_name (Thm_Name.short (extr_name name vs));
       in
         thy
         |> Sign.add_consts [(b, fastype_of ft, NoSyn)]
         |> Global_Theory.add_def
-           (Binding.qualified_name (Thm.def_name (extr_name s vs)), Logic.mk_equals (head, ft))
+           (Binding.qualified_name (Thm.def_name (Thm_Name.short (extr_name name vs))),
+             Logic.mk_equals (head, ft))
         |-> (fn def_thm =>
            Spec_Rules.add_global b Spec_Rules.equational
              [Thm.term_of (Thm.lhs_of def_thm)] [def_thm]
@@ -836,7 +847,7 @@
         val corr_prop = Proofterm.prop_of prf;
       in
         thy
-        |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
+        |> Global_Theory.store_thm (Binding.qualified_name (Thm_Name.short (corr_name s vs)),
             Thm.varifyT_global (funpow (length (vars_of corr_prop))
               (Thm.forall_elim_var 0) (Thm.forall_intr_frees
                 (Proof_Checker.thm_of_proof thy
@@ -845,7 +856,7 @@
       end;
 
     fun add_def_and_corr (s, (vs, ((t, u), (prf, _)))) thy =
-      if is_none (Sign.const_type thy (extr_name s vs))
+      if is_none (Sign.const_type thy (Thm_Name.short (extr_name s vs)))
       then
         thy
         |> not (t = nullt) ? add_def (s, (vs, ((t, u))))
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -85,8 +85,9 @@
               (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
           end;
 
-        fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) =
+        fun thm_of _ _ (PThm ({thm_name, prop = prop', types = SOME Ts, ...}, _)) =
               let
+                val name = Thm_Name.short thm_name;
                 val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
                 val prop = Thm.prop_of thm;
                 val _ =
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jun 07 23:53:31 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 ({name = "Pure.protectD", ...}, _) % _ %%
-        (PThm ({name = "Pure.protectI", ...}, _) % _ %% prf)) = SOME prf
-      | rew' (PThm ({name = "Pure.conjunctionD1", ...}, _) % _ % _ %%
-        (PThm ({name = "Pure.conjunctionI", ...}, _) % _ % _ %% prf %% _)) = SOME prf
-      | rew' (PThm ({name = "Pure.conjunctionD2", ...}, _) % _ % _ %%
-        (PThm ({name = "Pure.conjunctionI", ...}, _) % _ % _ %% _ %% 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 ({name = "Pure.protectI", ...}, _)) % _ %% 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 ({name = "Pure.protectI", ...}, _)) % _ %% 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,8 +245,8 @@
       (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
   | insert_refl defs Ts prf =
       (case Proofterm.strip_combt prf of
-        (PThm ({name = s, prop, types = SOME Ts, ...}, _), ts) =>
-          if member (op =) defs s then
+        (PThm ({thm_name, prop, types = SOME Ts, ...}, _), ts) =>
+          if member (op =) defs thm_name then
             let
               val vs = vars_of prop;
               val tvars = build_rev (Term.add_tvars 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, name, prop, ...}, _) =>
-                if member (op =) defnames name orelse
+            (fn PThm ({serial, 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, "")
+                else Inttab.update (serial, Thm_Name.empty)
               | _ => I) [prf] Inttab.empty;
         in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end
       else prf;
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Jun 07 23:53:31 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 -> string option} ->
+  val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.T option} ->
     thm -> Proofterm.proof
   val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
@@ -104,9 +104,11 @@
   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, name, types = Ts, ...}, _)) =
+fun term_of _ (PThm ({serial = i, thm_name = a, types = Ts, ...}, _)) =
       fold AppT (these Ts)
-        (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT))
+        (Const
+          (Long_Name.append "thm"
+            (if Thm_Name.is_empty a then string_of_int i else Thm_Name.short a), proofT))
   | term_of _ (PAxm (name, _, Ts)) =
       fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
   | term_of _ (PClass (T, c)) = AppT T (PClasst (T, c))
@@ -224,7 +226,8 @@
 fun proof_syntax prf =
   let
     val thm_names = Symset.dest (Proofterm.fold_proof_atoms true
-      (fn PThm ({name, ...}, _) => if name <> "" then Symset.insert name else I
+      (fn PThm ({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
       (fn PAxm (name, _, _) => Symset.insert name | _ => I) [prf] Symset.empty);
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Pure.thy	Fri Jun 07 23:53:31 2024 +0200
@@ -1386,7 +1386,7 @@
                 NONE => (Theory.parents_of thy, [thy])
               | SOME (xs, NONE) => (map check xs, [thy])
               | SOME (xs, SOME ys) => (map check xs, map check ys))
-            |> map pretty_thm |> Pretty.writeln_chunks
+            |> map (apfst Thm_Name.short #> pretty_thm) |> Pretty.writeln_chunks
           end)));
 
 in end\<close>
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/global_theory.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -29,7 +29,7 @@
   val official2: name_flags
   val unofficial1: name_flags
   val unofficial2: name_flags
-  val name_thm: name_flags -> string * Position.T -> thm -> thm
+  val name_thm: name_flags -> Thm_Name.P -> thm -> thm
   val name_thms: name_flags -> string * Position.T -> thm list -> thm list
   val name_facts: name_flags -> string * Position.T -> (thm list * 'a) list -> (thm list * 'a) list
   val check_thms_lazy: thm list lazy -> thm list lazy
@@ -251,21 +251,18 @@
       No_Name_Flags => thm
     | Name_Flags {post, official} =>
         thm
-        |> (official andalso (post orelse Thm.raw_derivation_name thm = "")) ?
+        |> (official andalso (post orelse Thm_Name.is_empty (Thm.raw_derivation_name thm))) ?
             Thm.name_derivation (name, pos)
-        |> (name <> "" andalso (post orelse not (Thm.has_name_hint thm))) ?
-            Thm.put_name_hint name));
+        |> (not (Thm_Name.is_empty name) andalso (post orelse not (Thm.has_name_hint thm))) ?
+            Thm.put_name_hint (Thm_Name.short name)));
 
 end;
 
-fun name_thm_short name_flags name =
-  name_thm name_flags (Thm_Name.short name);
-
 fun name_thms name_flags name_pos thms =
-  Thm_Name.list name_pos thms |> map (uncurry (name_thm_short name_flags));
+  Thm_Name.list name_pos thms |> map (uncurry (name_thm name_flags));
 
 fun name_facts name_flags name_pos facts =
-  Thm_Name.expr name_pos facts |> (map o apfst o map) (uncurry (name_thm_short name_flags));
+  Thm_Name.expr name_pos facts |> (map o apfst o map) (uncurry (name_thm name_flags));
 
 
 (* store theorems and proofs *)
@@ -319,7 +316,7 @@
         in ((thms', atts), thy2) end);
 
     val unnamed = #1 name = "";
-    val name_thm1 = if unnamed then #2 else uncurry (name_thm_short name_flags1);
+    val name_thm1 = if unnamed then #2 else uncurry (name_thm name_flags1);
 
     val app_facts =
       fold_maps (fn (named_thms, atts) => fn thy =>
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/proofterm.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -9,7 +9,7 @@
 signature PROOFTERM =
 sig
   type thm_header =
-    {serial: serial, pos: Position.T list, theory_name: string, name: string,
+    {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
       prop: term, types: typ list option}
   type thm_body
   type thm_node
@@ -38,13 +38,13 @@
   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 -> string -> term -> typ list option ->
+  val thm_header: serial -> Position.T list -> string -> Thm_Name.T -> term -> typ list option ->
     thm_header
   val thm_body: proof_body -> thm_body
   val thm_body_proof_raw: thm_body -> proof
   val thm_body_proof_open: thm_body -> proof
   val thm_node_theory_name: thm_node -> string
-  val thm_node_name: thm_node -> string
+  val thm_node_name: thm_node -> Thm_Name.T
   val thm_node_prop: thm_node -> term
   val thm_node_body: thm_node -> proof_body future
   val thm_node_thms: thm_node -> thm list
@@ -52,7 +52,7 @@
   val make_thm: thm_header -> thm_body -> thm
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms:
-    ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
+    ({serial: serial, thm_name: Thm_Name.T, prop: term, body: proof_body} -> 'a -> 'a) ->
     proof_body list -> 'a -> 'a
   val oracle_ord: oracle ord
   val thm_ord: thm ord
@@ -170,8 +170,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 -> string option
-  val expand_proof: theory -> (thm_header -> string option) -> proof -> proof
+  val expand_name_empty: thm_header -> Thm_Name.T option
+  val expand_proof: theory -> (thm_header -> Thm_Name.T option) -> proof -> proof
 
   val standard_vars: Name.context -> term * proof option -> term * proof option
   val standard_vars_term: Name.context -> term -> term
@@ -183,13 +183,13 @@
   val export_proof_boxes_required: theory -> bool
   val export_proof_boxes: proof_body list -> unit
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
-  val thm_proof: theory -> sorts_proof -> string * Position.T -> sort list -> term list ->
+  val thm_proof: theory -> sorts_proof -> Thm_Name.P -> sort list -> term list ->
     term -> (serial * proof_body future) list -> proof_body -> proof_body
   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, name: string} option
-  val get_approximative_name: sort list -> term list -> term -> proof -> string
+    {serial: serial, theory_name: string, thm_name: Thm_Name.T} option
+  val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.T
   type thm_id = {serial: serial, theory_name: string}
   val make_thm_id: serial * string -> thm_id
   val thm_header_id: thm_header -> thm_id
@@ -206,7 +206,7 @@
 (** datatype proof **)
 
 type thm_header =
-  {serial: serial, pos: Position.T list, theory_name: string, name: string,
+  {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
     prop: term, types: typ list option};
 
 datatype proof =
@@ -230,7 +230,7 @@
 and thm_body =
   Thm_Body of {open_proof: proof -> proof, body: proof_body future}
 and thm_node =
-  Thm_Node of {theory_name: string, name: string, prop: term,
+  Thm_Node of {theory_name: string, thm_name: Thm_Name.T, prop: term,
     body: proof_body future, export: unit lazy, consolidate: unit lazy};
 
 type oracle = (string * Position.T) * term option;
@@ -253,8 +253,9 @@
 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 name prop types : thm_header =
-  {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
+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,
+    prop = prop, types = types};
 
 fun thm_body body = Thm_Body {open_proof = I, body = Future.value body};
 fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body;
@@ -262,7 +263,7 @@
 
 fun rep_thm_node (Thm_Node args) = args;
 val thm_node_theory_name = #theory_name o rep_thm_node;
-val thm_node_name = #name o rep_thm_node;
+val thm_node_name = #thm_name o rep_thm_node;
 val thm_node_prop = #prop o rep_thm_node;
 val thm_node_body = #body o rep_thm_node;
 val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms);
@@ -276,21 +277,21 @@
   maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
   #> Lazy.consolidate #> map Lazy.force #> ignore;
 
-fun make_thm_node theory_name name prop body export =
+fun make_thm_node theory_name thm_name prop body export =
   let
     val consolidate =
       Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
         let val PBody {thms, ...} = Future.join body
         in consolidate_bodies (join_thms thms) end);
   in
-    Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body,
+    Thm_Node {theory_name = theory_name, thm_name = thm_name, prop = prop, body = body,
       export = export, consolidate = consolidate}
   end;
 
 val no_export = Lazy.value ();
 
-fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
-  (serial, make_thm_node theory_name name prop body no_export);
+fun make_thm ({serial, theory_name, thm_name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
+  (serial, make_thm_node theory_name thm_name prop body no_export);
 
 
 (* proof atoms *)
@@ -317,11 +318,11 @@
         if Intset.member seen i then (x, seen)
         else
           let
-            val name = thm_node_name thm_node;
+            val thm_name = thm_node_name thm_node;
             val prop = thm_node_prop thm_node;
             val body = Future.join (thm_node_body thm_node);
             val (x', seen') = app body (x, Intset.insert i seen);
-          in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
+          in (f {serial = i, thm_name = thm_name, prop = prop, body = body} x', seen') end);
   in fn bodies => fn x => #1 (fold app bodies (x, Intset.empty)) end;
 
 
@@ -341,8 +342,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, name = _, prop, types}, thm_body)) =
-      PThm (thm_header serial pos theory_name "" prop types, thm_body)
+  | 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 a = a;
 
 fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
@@ -385,8 +386,8 @@
   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, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
-    ([int_atom serial, theory_name, name],
+  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)))))]
@@ -394,7 +395,7 @@
   triple (list (pair (pair string (properties o Position.properties_of))
       (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
 and thm consts (a, thm_node) =
-  pair int (pair string (pair string (pair (term consts) (proof_body consts))))
+  pair int (pair string (pair (pair string int) (pair (term consts) (proof_body consts))))
     (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
       (Future.join (thm_node_body thm_node))))));
 
@@ -417,8 +418,8 @@
   fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
   fn PClass (T, c) => ([c], typ T),
   fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)),
-  fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
-    ([int_atom serial, theory_name, name], list typ Ts)];
+  fn PThm ({serial, theory_name, thm_name, types = SOME Ts, ...}, _) =>
+    ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)], list typ Ts)];
 
 in
 
@@ -447,12 +448,12 @@
   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) =>
+  fn ([a, b, c, d], e) =>
     let
-      val ((e, (f, (g, h)))) =
-        pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) d;
-      val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
-    in PThm (header, thm_body h) end]
+      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]
 and proof_body consts x =
   let
     val (a, b, c) =
@@ -462,7 +463,7 @@
 and thm consts x =
   let
     val (a, (b, (c, (d, e)))) =
-      pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x
+      pair int (pair string (pair (pair string int) (pair (term consts) (proof_body consts)))) x
   in (a, make_thm_node b c d (Future.value e) no_export) end;
 
 in
@@ -556,8 +557,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, name, prop, types = SOME Ts}, thm_body)) =
-          PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body)
+      | 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 _ = raise Same.SAME;
   in proof end;
 
@@ -597,8 +598,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, name, prop, types = _}, thm_body)) =
-      PThm (thm_header serial pos theory_name name prop types, thm_body)
+  | 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 _ prf = prf;
 
 
@@ -762,8 +763,8 @@
           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, name = a, prop = t, types = Ts}, thm_body)) =
-          PThm (thm_header i p theory_name a t
+      | norm (PThm ({serial = i, 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;
   in Same.commit norm end;
@@ -1023,8 +1024,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, name, prop, types}, thm_body)) =
-          PThm (thm_header serial pos theory_name name prop (typs types), thm_body)
+      | 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 _ _ _ = raise Same.SAME;
 
     val k = length prems;
@@ -1399,8 +1400,8 @@
           if c1 = c2 then matchT inst (T1, T2)
           else raise PMatch
       | mtch Ts i j inst
-            (PThm ({name = name1, prop = prop1, types = types1, ...}, _),
-              PThm ({name = name2, prop = prop2, types = types2, ...}, _)) =
+            (PThm ({thm_name = name1, prop = prop1, types = types1, ...}, _),
+              PThm ({thm_name = name2, prop = prop2, types = types2, ...}, _)) =
           if name1 = name2 andalso prop1 = prop2
           then optmatch matchTs inst (types1, types2)
           else raise PMatch
@@ -1446,8 +1447,8 @@
       | 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, name = id, prop, types}, thm_body)) =
-          PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body)
+      | subst _ _ (PThm ({serial = i, 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;
 
@@ -1466,7 +1467,7 @@
       | (Hyp (Var _), _) => true
       | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
       | (PClass (_, c), PClass (_, d)) => c = d andalso matchrands prf1 prf2
-      | (PThm ({name = a, prop = propa, ...}, _), PThm ({name = b, prop = propb, ...}, _)) =>
+      | (PThm ({thm_name = a, prop = propa, ...}, _), PThm ({thm_name = b, prop = propb, ...}, _)) =>
           a = b andalso propa = propb andalso matchrands prf1 prf2
       | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
       | (AbsP _, _) =>  true   (*because of possible eta equality*)
@@ -1616,12 +1617,12 @@
         (fn TVar ((a, i), S) => subst_same (TVar ((a, i - shift), S)) | A => subst_same A);
   in Same.commit (map_proof_types_same subst_type_same) prf end;
 
-fun guess_name (PThm ({name, ...}, _)) = name
+fun guess_name (PThm ({thm_name, ...}, _)) = thm_name
   | guess_name (prf %% Hyp _) = guess_name prf
   | guess_name (prf %% PClass _) = guess_name prf
   | guess_name (prf % NONE) = guess_name prf
   | guess_name (prf % SOME (Var _)) = guess_name prf
-  | guess_name _ = "";
+  | guess_name _ = Thm_Name.empty;
 
 
 (* generate constraints for proof term *)
@@ -1733,7 +1734,7 @@
               | 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 (guess_name prf))
+                error ("Wrong number of type arguments for " ^ quote (Thm_Name.short (guess_name prf)))
           in (prop', change_types (SOME Ts) prf, [], env', vTs) end;
 
     fun head_norm (prop, prf, cnstrts, env, vTs) =
@@ -1920,7 +1921,8 @@
 
 (* expand and reconstruct subproofs *)
 
-fun expand_name_empty (header: thm_header) = if #name header = "" then SOME "" else NONE;
+fun expand_name_empty (header: thm_header) =
+  if Thm_Name.is_empty (#thm_name header) then SOME Thm_Name.empty else NONE;
 
 fun expand_proof thy expand_name prf =
   let
@@ -1939,10 +1941,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, name, prop, types} = header in
+          let val {serial, pos, theory_name, thm_name, prop, types} = header in
             (case expand_name header of
-              SOME name' =>
-                if name' = "" andalso is_some types then
+              SOME thm_name' =>
+                if #1 thm_name' = "" andalso is_some types then
                   let
                     val (seen', maxidx', prf') =
                       (case Inttab.lookup seen serial of
@@ -1959,8 +1961,9 @@
                     val prf'' = prf'
                       |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop (the types);
                   in (seen', maxidx' + maxidx + 1, prf'') end
-                else if name' <> name then
-                  (seen, maxidx, PThm (thm_header serial pos theory_name name' prop types, thm_body))
+                else if thm_name' <> thm_name then
+                  (seen, maxidx,
+                    PThm (thm_header serial pos theory_name thm_name' prop types, thm_body))
                 else (seen, maxidx, prf)
             | NONE => (seen, maxidx, prf))
           end
@@ -2173,7 +2176,7 @@
     (name, pos) shyps hyps concl promises
     (PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zproof0, proof = proof0}) =
   let
-    val named = name <> "";
+    val named = not (Thm_Name.is_empty name);
 
     val prop = Logic.list_implies (hyps, concl);
     val args = prop_args prop;
@@ -2203,11 +2206,11 @@
       if export_enabled () then new_prf ()
       else
         (case strip_combt (proof_head_of proof0) of
-          (PThm ({serial = ser, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
-            if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
+          (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';
-                val i = if a = "" andalso named then serial () else ser;
+                val i = if #1 a = "" andalso named then serial () else ser;
               in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end
             else new_prf ()
         | _ => new_prf ());
@@ -2257,7 +2260,7 @@
   prepare_thm_proof false thy sorts_proof name shyps hyps concl promises #> #2;
 
 fun unconstrain_thm_proof thy sorts_proof shyps concl promises body =
-  prepare_thm_proof true thy sorts_proof ("", Position.none)
+  prepare_thm_proof true thy sorts_proof Thm_Name.none
     shyps [] concl promises body;
 
 end;
@@ -2268,14 +2271,14 @@
 fun get_identity shyps hyps prop prf =
   let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
     (case term_head_of (proof_head_of prf) of
-      PThm ({serial, theory_name, name, prop = prop', ...}, _) =>
+      PThm ({serial, theory_name, thm_name, prop = prop', ...}, _) =>
         if prop = prop'
-        then SOME {serial = serial, theory_name = theory_name, name = name} else NONE
+        then SOME {serial = serial, theory_name = theory_name, thm_name = thm_name} else NONE
     | _ => NONE)
   end;
 
 fun get_approximative_name shyps hyps prop prf =
-  Option.map #name (get_identity shyps hyps prop prf) |> the_default "";
+  Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.empty;
 
 
 (* thm_id *)
@@ -2294,8 +2297,8 @@
 fun get_id shyps hyps prop prf : thm_id option =
   (case get_identity shyps hyps prop prf of
     NONE => NONE
-  | SOME {name = "", ...} => NONE
-  | SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name)));
+  | SOME {serial, theory_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
   | this_id (SOME (thm_id: thm_id)) (thm_id': thm_id) = #serial thm_id = #serial thm_id';
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/term.scala
--- a/src/Pure/term.scala	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/term.scala	Fri Jun 07 23:53:31 2024 +0200
@@ -142,8 +142,8 @@
     private lazy val hash: Int = ("Oracle", name, prop, types).hashCode()
     override def hashCode(): Int = hash
   }
-  case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof {
-    private lazy val hash: Int = ("PThm", serial, theory_name, name, types).hashCode()
+  case class PThm(serial: Long, theory_name: String, thm_name: Thm_Name, types: List[Typ]) extends Proof {
+    private lazy val hash: Int = ("PThm", serial, theory_name, thm_name, types).hashCode()
     override def hashCode(): Int = hash
   }
 
@@ -234,6 +234,10 @@
       }
     }
 
+    protected def cache_thm_name(x: Thm_Name): Thm_Name =
+      if (x == Thm_Name.empty) Thm_Name.empty
+      else lookup(x) getOrElse store(Thm_Name(cache_string(x.name), x.index))
+
     protected def cache_proof(x: Proof): Proof = {
       if (x == MinProof) MinProof
       else {
@@ -253,8 +257,9 @@
               case PClass(typ, cls) => store(PClass(cache_typ(typ), cache_string(cls)))
               case Oracle(name, prop, types) =>
                 store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
-              case PThm(serial, theory_name, name, types) =>
-                store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
+              case PThm(serial, theory_name, thm_name, types) =>
+                store(PThm(serial, cache_string(theory_name), cache_thm_name(thm_name),
+                  cache_typs(types)))
             }
         }
       }
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/term_xml.scala	Fri Jun 07 23:53:31 2024 +0200
@@ -92,7 +92,9 @@
           { case (List(a), b) => PAxm(a, list(typ)(b)) },
           { case (List(a), b) => PClass(typ(b), a) },
           { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
-          { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
+          { case (List(a, b, c, d), e) =>
+            PThm(long_atom(a), b, Thm_Name(c, int_atom(d)), list(typ)(e))
+          }))
       proof
     }
 
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -118,11 +118,11 @@
   val extra_shyps: thm -> sort list
   val strip_shyps: thm -> thm
   val derivation_closed: thm -> bool
-  val derivation_name: thm -> string
+  val derivation_name: thm -> Thm_Name.T
   val derivation_id: thm -> Proofterm.thm_id option
-  val raw_derivation_name: thm -> string
-  val expand_name: thm -> Proofterm.thm_header -> string option
-  val name_derivation: string * Position.T -> thm -> thm
+  val raw_derivation_name: thm -> Thm_Name.T
+  val expand_name: thm -> Proofterm.thm_header -> Thm_Name.T option
+  val name_derivation: Thm_Name.P -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
   val axiom: theory -> string -> thm
@@ -1130,7 +1130,9 @@
       (case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of
         NONE => K false
       | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header);
-    fun expand header = if self_id header orelse #name header = "" then SOME "" else NONE;
+    fun expand header =
+      if self_id header orelse Thm_Name.is_empty (#thm_name header)
+      then SOME Thm_Name.empty else NONE;
   in expand end;
 
 (*deterministic name of finished proof*)
@@ -1166,7 +1168,7 @@
 fun close_derivation pos =
   solve_constraints #> (fn thm =>
     if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
-    else name_derivation ("", pos) thm);
+    else name_derivation (Thm_Name.empty, pos) thm);
 
 val trim_context = solve_constraints #> trim_context_thm;
 
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/thm_deps.ML
--- a/src/Pure/thm_deps.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm_deps.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -12,7 +12,7 @@
   val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
   val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list
   val pretty_thm_deps: theory -> thm list -> Pretty.T
-  val unused_thms_cmd: theory list * theory list -> (string * thm) list
+  val unused_thms_cmd: theory list * theory list -> (Thm_Name.T * thm) list
 end;
 
 structure Thm_Deps: THM_DEPS =
@@ -96,9 +96,8 @@
       else
         let val {concealed, group, ...} = Name_Space.the_entry space name in
           fold_rev (transfer #> (fn th =>
-            (case Thm.derivation_name th of
-              "" => I
-            | a => cons (a, (th, concealed, group))))) ths
+            let val a = Thm.derivation_name th
+            in if Thm_Name.is_empty a then I else cons (a, (th, concealed, group)) end)) ths
         end;
     fun add_facts thy =
       let
@@ -108,15 +107,15 @@
 
     val new_thms =
       fold add_facts thys []
-      |> sort_distinct (string_ord o apply2 #1);
+      |> sort_distinct (Thm_Name.ord o apply2 #1);
 
     val used =
       Proofterm.fold_body_thms
-        (fn {name = a, ...} => a <> "" ? Symset.insert a)
+        (fn {thm_name = a, ...} => not (Thm_Name.is_empty a) ? Thm_Name.Set.insert a)
         (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
-        Symset.empty;
+        Thm_Name.Set.empty;
 
-    fun is_unused a = not (Symset.member used a);
+    fun is_unused a = not (Thm_Name.Set.member used a);
 
     (*groups containing at least one used theorem*)
     val used_groups =
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm_name.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -11,10 +11,14 @@
 sig
   type T = string * int
   val ord: T ord
+  structure Set: SET
+  structure Table: TABLE
+  val empty: T
+  val is_empty: T -> bool
+  val print: T -> string
+  val short: T -> string
   type P = T * Position.T
   val none: P
-  val print: T -> string
-  val short: P -> string * Position.T
   val list: string * Position.T -> 'a list -> (P * 'a) list
   val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list
 end;
@@ -25,19 +29,27 @@
 type T = string * int;
 val ord = prod_ord string_ord int_ord;
 
-type P = T * Position.T;
+structure Set = Set(type key = T val ord = ord);
+structure Table = Table(Set.Key);
 
-val none: P = (("", 0), Position.none);
+val empty: T = ("", 0);
+fun is_empty ((a, _): T) = a = "";
 
 fun print (name, index) =
   if name = "" orelse index = 0 then name
   else name ^ enclose "(" ")" (string_of_int index);
 
-fun short (((name, index), pos): P) =
-  if name = "" orelse index = 0 then (name, pos)
-  else (name ^ "_" ^ string_of_int index, pos);
+fun short (name, index) =
+  if name = "" orelse index = 0 then name
+  else name ^ "_" ^ string_of_int index;
+
+
+type P = T * Position.T;
+
+val none: P = (empty, Position.none);
 
 fun list (name, pos) [thm] = [(((name, 0), pos): P, thm)]
+  | list ("", pos) thms = map (fn thm => ((empty, pos), thm)) thms
   | list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms;
 
 fun expr name = burrow_fst (burrow (list name));
diff -r eec06d39e5fa -r 8a9588ffc133 src/Pure/thm_name.scala
--- a/src/Pure/thm_name.scala	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm_name.scala	Fri Jun 07 23:53:31 2024 +0200
@@ -23,6 +23,8 @@
 
   private val Thm_Name_Regex = """^(.)+\((\d+)\)$""".r
 
+  val empty: Thm_Name = Thm_Name("", 0)
+
   def parse(s: String): Thm_Name =
     s match {
       case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
@@ -31,6 +33,8 @@
 }
 
 sealed case class Thm_Name(name: String, index: Int) {
+  def is_empty: Boolean = name.isEmpty
+
   def print: String =
     if (name == "" || index == 0) name
     else name + "(" + index + ")"