tuned signature: more operations;

--- a/src/Pure/General/name_space.ML	Sun Dec 01 21:14:56 2024 +0100
+++ b/src/Pure/General/name_space.ML	Sun Dec 01 21:46:54 2024 +0100
@@ -29,6 +29,7 @@
   val names_short: bool Config.T
   val names_unique: bool Config.T
   val extern_generic: Context.generic -> T -> string -> xstring
+  val extern_global: theory -> T -> string -> xstring
   val extern: Proof.context -> T -> string -> xstring
   val extern_ord: Proof.context -> T -> string ord
   val extern_shortest: Proof.context -> T -> string -> xstring
@@ -322,6 +323,7 @@
     else extern_names (get_aliases space name)
   end;
 
+val extern_global = extern_generic o Context.Theory;
 val extern = extern_generic o Context.Proof;
 
 fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);

--- a/src/Pure/Isar/locale.ML	Sun Dec 01 21:14:56 2024 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Dec 01 21:46:54 2024 +0100
@@ -199,8 +199,7 @@
    (Args.theory -- Scan.lift Parse.embedded_position >>
       (ML_Syntax.print_string o uncurry check)));
 
-fun extern thy =
-  Name_Space.extern_generic (Context.Theory thy) (locale_space thy);
+fun extern thy = Name_Space.extern_global thy (locale_space thy);
 
 fun markup_extern ctxt =
   Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt));

--- a/src/Pure/thm_deps.ML	Sun Dec 01 21:14:56 2024 +0100
+++ b/src/Pure/thm_deps.ML	Sun Dec 01 21:46:54 2024 +0100
@@ -74,7 +74,7 @@
 fun pretty_thm_deps thy thms =
   let
     val facts = Global_Theory.facts_of thy;
-    val extern_fact = Name_Space.extern_generic (Context.Theory thy) (Facts.space_of facts);
+    val extern_fact = Name_Space.extern_global thy (Facts.space_of facts);
     val deps =
       (case try (thm_deps thy) thms of
         SOME deps => deps