more accurate output of Thm_Name.T wrt. facts name space;

--- a/src/Pure/Isar/proof_context.ML	Sat Jun 08 11:47:48 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jun 08 16:26:47 2024 +0200
@@ -62,6 +62,8 @@
   val facts_of: Proof.context -> Facts.T
   val facts_of_fact: Proof.context -> string -> Facts.T
   val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring
+  val pretty_thm_name: Proof.context -> Thm_Name.T -> Pretty.T
+  val print_thm_name: Proof.context -> Thm_Name.T -> string
   val augment: term -> Proof.context -> Proof.context
   val print_name: Proof.context -> string -> string
   val pretty_name: Proof.context -> string -> Pretty.T
@@ -423,6 +425,11 @@
       else [markup];
   in (markups, xname) end;
 
+fun pretty_thm_name ctxt (name, i) =
+  Facts.pretty_thm_name (Context.Proof ctxt) (facts_of_fact ctxt name) (name, i);
+
+val print_thm_name = Pretty.string_of oo pretty_thm_name;
+
 
 (* augment context by implicit term declarations *)
 

--- a/src/Pure/Proof/extraction.ML	Sat Jun 08 11:47:48 2024 +0200
+++ b/src/Pure/Proof/extraction.ML	Sat Jun 08 16:26:47 2024 +0200
@@ -641,7 +641,7 @@
                     val _ = T = nullT orelse error "corr: internal error";
                     val _ =
                       msg d ("Building correctness proof for " ^
-                        quote (Thm_Name.short thm_name) ^
+                        quote (Global_Theory.print_thm_name thy thm_name) ^
                         (if null vs' then ""
                          else " (relevant variables: " ^ commas_quote vs' ^ ")"));
                     val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
@@ -670,7 +670,7 @@
             | 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 (Thm_Name.short thm_name) ^ ":\n" ^
+                  quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^
                     Syntax.string_of_term_global thy'
                       (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
           end
@@ -738,7 +738,7 @@
                 NONE =>
                   let
                     val _ =
-                      msg d ("Extracting " ^ quote (Thm_Name.short thm_name) ^
+                      msg d ("Extracting " ^ quote (Global_Theory.print_thm_name thy' thm_name) ^
                         (if null vs' then ""
                          else " (relevant variables: " ^ commas_quote vs' ^ ")"));
                     val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
@@ -790,7 +790,7 @@
             | SOME rs => (case find vs' rs of
                 SOME (t, _) => (subst_TVars tye' t, defs)
               | NONE => error ("extr: no realizer for instance of theorem " ^
-                  quote (Thm_Name.short thm_name) ^ ":\n" ^
+                  quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^
                     Syntax.string_of_term_global thy' (Envir.beta_norm
                     (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))
           end
@@ -817,7 +817,7 @@
         val name = Thm.derivation_name thm;
         val _ = if Thm_Name.is_empty name then error "extraction: unnamed theorem" else ();
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
-          quote (Thm_Name.short name) ^ " has no computational content")
+          quote (Global_Theory.print_thm_name thy' name) ^ " has no computational content")
       in Proofterm.reconstruct_proof thy' prop prf end;
 
     val defs =

--- a/src/Pure/Proof/proof_checker.ML	Sat Jun 08 11:47:48 2024 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Sat Jun 08 16:26:47 2024 +0200
@@ -93,7 +93,8 @@
                 val _ =
                   if is_equal prop prop' then ()
                   else
-                    error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
+                    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');
               in thm_of_atom thm Ts end

--- a/src/Pure/Pure.thy	Sat Jun 08 11:47:48 2024 +0200
+++ b/src/Pure/Pure.thy	Sat Jun 08 16:26:47 2024 +0200
@@ -1378,7 +1378,9 @@
           let
             val thy = Toplevel.theory_of st;
             val ctxt = Toplevel.context_of st;
-            fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
+            fun pretty_thm (a, th) =
+              Pretty.block [Pretty.quote (Proof_Context.pretty_thm_name ctxt a),
+                Pretty.str ":", Pretty.brk 1, Thm.pretty_thm ctxt th];
             val check = Theory.check {long = false} ctxt;
           in
             Thm_Deps.unused_thms_cmd
@@ -1386,7 +1388,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 (apfst Thm_Name.short #> pretty_thm) |> Pretty.writeln_chunks
+            |> map pretty_thm |> Pretty.writeln_chunks
           end)));
 
 in end\<close>

--- a/src/Pure/facts.ML	Sat Jun 08 11:47:48 2024 +0200
+++ b/src/Pure/facts.ML	Sat Jun 08 16:26:47 2024 +0200
@@ -30,6 +30,7 @@
   val intern: T -> xstring -> string
   val extern: Proof.context -> T -> string -> xstring
   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
+  val pretty_thm_name: Context.generic -> T -> Thm_Name.T -> Pretty.T
   val defined: T -> string -> bool
   val is_dynamic: T -> string -> bool
   val lookup: Context.generic -> T -> string -> {dynamic: bool, thms: thm list} option
@@ -173,6 +174,12 @@
 fun extern ctxt = Name_Space.extern ctxt o space_of;
 fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of;
 
+fun pretty_thm_name context facts thm_name =
+  let
+    val prfx = Thm_Name.print_prefix context (space_of facts) thm_name;
+    val sffx = Thm_Name.print_suffix thm_name;
+  in Pretty.block [Pretty.mark_str prfx, Pretty.str sffx] end;
+
 
 (* retrieve *)
 

--- a/src/Pure/global_theory.ML	Sat Jun 08 11:47:48 2024 +0200
+++ b/src/Pure/global_theory.ML	Sat Jun 08 16:26:47 2024 +0200
@@ -14,6 +14,8 @@
   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 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
@@ -67,7 +69,7 @@
 );
 
 
-(* facts *)
+(* global facts *)
 
 val facts_of = #1 o Data.get;
 val map_facts = Data.map o apfst;
@@ -86,6 +88,9 @@
   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));
 
+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;
+
 
 (* thm_name vs. derivation_id *)
 
@@ -104,8 +109,8 @@
           (case Inttab.lookup thm_names serial of
             SOME thm_name' =>
               raise THM ("Duplicate use of derivation identity for " ^
-                Thm_Name.print thm_name ^ " vs. " ^
-                Thm_Name.print thm_name', 0, [thm])
+                print_thm_name thy thm_name ^ " vs. " ^
+                print_thm_name thy thm_name', 0, [thm])
           | NONE => Inttab.update (serial, thm_name) thm_names)));
 
 fun lazy_thm_names thy =

--- a/src/Pure/proofterm.ML	Sat Jun 08 11:47:48 2024 +0200
+++ b/src/Pure/proofterm.ML	Sat Jun 08 16:26:47 2024 +0200
@@ -1734,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 (Thm_Name.short (guess_name prf)))
+                error ("Wrong number of type arguments for " ^ quote (Thm_Name.print (guess_name prf)))
           in (prop', change_types (SOME Ts) prf, [], env', vTs) end;
 
     fun head_norm (prop, prf, cnstrts, env, vTs) =

--- a/src/Pure/thm_deps.ML	Sat Jun 08 11:47:48 2024 +0200
+++ b/src/Pure/thm_deps.ML	Sat Jun 08 16:26:47 2024 +0200
@@ -73,17 +73,17 @@
 
 fun pretty_thm_deps thy thms =
   let
-    val ctxt = Proof_Context.init_global thy;
+    val facts = Global_Theory.facts_of thy;
+    val extern_fact = Name_Space.extern_generic (Context.Theory thy) (Facts.space_of facts);
     val deps =
       (case try (thm_deps thy) thms of
         SOME deps => deps
       | NONE => error "Malformed proofs");
     val items =
-      map #2 deps
-      |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i))
-      |> sort_by (#2 o #1)
-      |> map (fn ((marks, xname), i) =>
-          Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]);
+      deps
+      |> map (fn (_, thm_name as (name, _)) => (extern_fact name, thm_name))
+      |> sort_by #1
+      |> map (fn (_, thm_name) => Pretty.item [Global_Theory.pretty_thm_name thy thm_name])
   in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;
 
 

--- a/src/Pure/thm_name.ML	Sat Jun 08 11:47:48 2024 +0200
+++ b/src/Pure/thm_name.ML	Sat Jun 08 16:26:47 2024 +0200
@@ -21,6 +21,8 @@
   val list: string * Position.T -> 'a list -> (P * 'a) list
   val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list
 
+  val print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string
+  val print_suffix: T -> string
   val print: T -> string
   val short: T -> string
 end;
@@ -55,9 +57,15 @@
 
 (* output *)
 
-fun print (name, index) =
-  if name = "" orelse index = 0 then name
-  else name ^ enclose "(" ")" (string_of_int index);
+fun print_prefix context space ((name, _): T) =
+  if name = "" then (Markup.empty, "")
+  else (Name_Space.markup space name, Name_Space.extern_generic context space name);
+
+fun print_suffix (name, index) =
+  if name = "" orelse index = 0 then ""
+  else enclose "(" ")" (string_of_int index);
+
+fun print (name, index) = name ^ print_suffix (name, index);
 
 fun short (name, index) =
   if name = "" orelse index = 0 then name