# HG changeset patch
# User wenzelm
# Date 1733136342 -3600
# Node ID aed257e030d235120706f114f4e1dcc96727ec2b
# Parent  db073d1733ab5528a8b0f18bb0b687c899a68a85
clarified signature: uniform context;

diff -r db073d1733ab -r aed257e030d2 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Dec 02 11:36:53 2024 +0100
+++ b/src/Pure/General/name_space.ML	Mon Dec 02 11:45:42 2024 +0100
@@ -28,8 +28,6 @@
   val names_long: bool Config.T
   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
@@ -293,11 +291,11 @@
 val names_short = Config.declare_option_bool ("names_short", \<^here>);
 val names_unique = Config.declare_option_bool ("names_unique", \<^here>);
 
-fun extern_generic context space name =
+fun extern ctxt space name =
   let
-    val names_long = Config.get_generic context names_long;
-    val names_short = Config.get_generic context names_short;
-    val names_unique = Config.get_generic context names_unique;
+    val names_long = Config.get ctxt names_long;
+    val names_short = Config.get ctxt names_short;
+    val names_unique = Config.get ctxt names_unique;
 
     fun extern_chunks require_unique a chunks =
       let val {full_name = c, unique, ...} = intern_chunks space chunks in
@@ -323,9 +321,6 @@
     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);
 
 fun extern_shortest ctxt =