# HG changeset patch
# User wenzelm
# Date 1681987459 -7200
# Node ID f4cd6e3b5075d2e3fc69da453684e438b4f92a29
# Parent  26d49c15bff00fdab693092f512438bbc12e227b
prefer theory_long_name in data;

diff -r 26d49c15bff0 -r f4cd6e3b5075 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Apr 20 12:23:41 2023 +0200
+++ b/src/Pure/thm.ML	Thu Apr 20 12:44:19 2023 +0200
@@ -179,7 +179,7 @@
   val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
     bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
-  val thynames_of_arity: theory -> string * class -> string list
+  val theory_names_of_arity: {long: bool} -> theory -> string * class -> string list
   val add_classrel: thm -> theory -> theory
   val add_arity: thm -> theory -> theory
 end;
@@ -2343,10 +2343,10 @@
 
 (* type arities *)
 
-fun thynames_of_arity thy (a, c) =
+fun theory_names_of_arity {long} thy (a, c) =
   build (get_arities thy |> Aritytab.fold
     (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)))
-  |> sort (int_ord o apply2 #2) |> map #1;
+  |> sort (int_ord o apply2 #2) |> map (if long then #1 else Long_Name.base_name o #1);
 
 fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) =
   let
@@ -2404,7 +2404,7 @@
     val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context;
     val prop = plain_prop_of th;
     val (t, Ss, c) = Logic.dest_arity prop;
-    val ar = ((t, Ss, c), (th', Context.theory_base_name thy, serial ()));
+    val ar = ((t, Ss, c), (th', Context.theory_long_name thy, serial ()));
   in
     thy
     |> Sign.primitive_arity (t, Ss, [c])
diff -r 26d49c15bff0 -r f4cd6e3b5075 src/Tools/Code/code_symbol.ML
--- a/src/Tools/Code/code_symbol.ML	Thu Apr 20 12:23:41 2023 +0200
+++ b/src/Tools/Code/code_symbol.ML	Thu Apr 20 12:44:19 2023 +0200
@@ -99,7 +99,7 @@
 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;
-  fun thyname_of_instance thy inst = case Thm.thynames_of_arity thy inst
+  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;
   fun thyname_of_const thy c = case Axclass.class_of_param thy c