# HG changeset patch
# User wenzelm
# Date 1683280869 -7200
# Node ID 6bb2f9b3280498a0b4c1a98fbc0f461c0b4ef9e4
# Parent  fa3474ed80bea477184e182ff296ce7245b8cbf4
clarified signature;

diff -r fa3474ed80be -r 6bb2f9b32804 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri May 05 11:52:53 2023 +0200
+++ b/src/Pure/General/name_space.ML	Fri May 05 12:01:09 2023 +0200
@@ -23,7 +23,7 @@
   val markup_def: T -> string -> Markup.T
   val get_names: T -> string list
   val the_entry: T -> string -> entry
-  val the_entry_theory_name: T -> string -> string
+  val theory_name: {long: bool} -> T -> string -> string
   val entry_ord: T -> string ord
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
@@ -260,8 +260,9 @@
     NONE => error (undefined space name)
   | SOME entry => entry);
 
-fun the_entry_theory_name space name =
-  Long_Name.base_name (#theory_long_name (the_entry space name));
+fun theory_name {long} space name =
+  #theory_long_name (the_entry space name)
+  |> not long ? Long_Name.base_name;
 
 fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
 
diff -r fa3474ed80be -r 6bb2f9b32804 src/Tools/Code/code_symbol.ML
--- a/src/Tools/Code/code_symbol.ML	Fri May 05 11:52:53 2023 +0200
+++ b/src/Tools/Code/code_symbol.ML	Fri May 05 12:01:09 2023 +0200
@@ -97,8 +97,9 @@
 end;
 
 local
-  val thyname_of_type = Name_Space.the_entry_theory_name o Sign.type_space;
-  val thyname_of_class = Name_Space.the_entry_theory_name o Sign.class_space;
+  val thyname_of = Name_Space.theory_name {long = false};
+  val thyname_of_type = thyname_of o Sign.type_space;
+  val thyname_of_class = thyname_of o Sign.class_space;
   fun thyname_of_instance thy inst = case Thm.theory_names_of_arity {long = false} thy inst
    of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^  snd inst))
     | thyname :: _ => thyname;
@@ -106,7 +107,7 @@
    of SOME class => thyname_of_class thy class
     | NONE => (case Code.get_type_of_constr_or_abstr thy c
        of SOME (tyco, _) => thyname_of_type thy tyco
-        | NONE => Name_Space.the_entry_theory_name (Sign.const_space thy) c);
+        | NONE => thyname_of (Sign.const_space thy) c);
   fun prefix thy (Constant "") = "Code"
     | prefix thy (Constant c) = thyname_of_const thy c
     | prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco