clarified modules: more direct data implementation;

--- a/src/Pure/axclass.ML	Mon Aug 05 11:20:56 2019 +0200
+++ b/src/Pure/axclass.ML	Mon Aug 05 16:11:43 2019 +0200
@@ -9,6 +9,7 @@
 sig
   type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
   val get_info: theory -> class -> info
+  val get_arity_thyname: theory -> string * class -> string option
   val class_of_param: theory -> string -> class option
   val instance_name: string * class -> string
   val param_of_inst: theory -> string * string -> string
@@ -67,59 +68,67 @@
 
 datatype data = Data of
  {axclasses: info Symtab.table,
+  arity_thynames: string Symreltab.table,
   params: param list,
-    (*arity theorems with theory name*)
   inst_params:
     (string * thm) Symtab.table Symtab.table *
       (*constant name ~> type constructor ~> (constant name, equation)*)
     (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*)};
 
-fun make_data (axclasses, params, inst_params) =
-  Data {axclasses = axclasses, params = params, inst_params = inst_params};
+fun make_data (axclasses, arity_thynames, params, inst_params) =
+  Data {axclasses = axclasses, arity_thynames = arity_thynames,
+    params = params, inst_params = inst_params};
 
 structure Data = Theory_Data'
 (
   type T = data;
-  val empty = make_data (Symtab.empty, [], (Symtab.empty, Symtab.empty));
+  val empty = make_data (Symtab.empty, Symreltab.empty, [], (Symtab.empty, Symtab.empty));
   val extend = I;
   fun merge old_thys
-      (Data {axclasses = axclasses1, params = params1, inst_params = inst_params1},
-       Data {axclasses = axclasses2, params = params2, inst_params = inst_params2}) =
+      (Data {axclasses = axclasses1, arity_thynames = arity_thynames1,
+          params = params1, inst_params = inst_params1},
+       Data {axclasses = axclasses2, arity_thynames = arity_thynames2,
+         params = params2, inst_params = inst_params2}) =
     let
       val old_ctxt = Syntax.init_pretty_global (fst old_thys);
 
       val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
+      val arity_thynames' = Symreltab.merge (K true) (arity_thynames1, arity_thynames2);
       val params' =
         if null params1 then params2
         else
           fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p)
             params2 params1;
-
       val inst_params' =
         (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
           Symtab.merge (K true) (#2 inst_params1, #2 inst_params2));
-    in make_data (axclasses', params', inst_params') end;
+    in make_data (axclasses', arity_thynames', params', inst_params') end;
 );
 
 fun map_data f =
-  Data.map (fn Data {axclasses, params, inst_params} =>
-    make_data (f (axclasses, params, inst_params)));
+  Data.map (fn Data {axclasses, arity_thynames, params, inst_params} =>
+    make_data (f (axclasses, arity_thynames, params, inst_params)));
 
 fun map_axclasses f =
-  map_data (fn (axclasses, params, inst_params) =>
-    (f axclasses, params, inst_params));
+  map_data (fn (axclasses, arity_thynames, params, inst_params) =>
+    (f axclasses, arity_thynames, params, inst_params));
+
+fun map_arity_thynames f =
+  map_data (fn (axclasses, arity_thynames, params, inst_params) =>
+    (axclasses, f arity_thynames, params, inst_params));
 
 fun map_params f =
-  map_data (fn (axclasses, params, inst_params) =>
-    (axclasses, f params, inst_params));
+  map_data (fn (axclasses, arity_thynames, params, inst_params) =>
+    (axclasses, arity_thynames, f params, inst_params));
 
 fun map_inst_params f =
-  map_data (fn (axclasses, params, inst_params) =>
-    (axclasses, params, f inst_params));
+  map_data (fn (axclasses, arity_thynames, params, inst_params) =>
+    (axclasses, arity_thynames, params, f inst_params));
 
 val rep_data = Data.get #> (fn Data args => args);
 
 val axclasses_of = #axclasses o rep_data;
+val arity_thynames_of = #arity_thynames o rep_data;
 val params_of = #params o rep_data;
 val inst_params_of = #inst_params o rep_data;
 
@@ -142,6 +151,18 @@
 fun class_of_param thy = AList.lookup (op =) (params_of thy);
 
 
+(* theory name of first type instantiation *)
+
+fun get_arity_thyname thy (t, c) =
+  get_first (fn c' => Symreltab.lookup (arity_thynames_of thy) (t, c'))
+    (c :: Sign.super_classes thy c);
+
+fun put_arity_thyname ar thy =
+  if is_some (get_arity_thyname thy ar) then thy
+  else map_arity_thynames (Symreltab.update (ar, Context.theory_name thy)) thy;
+
+
+
 (* maintain instance parameters *)
 
 fun get_inst_param thy (c, tyco) =
@@ -290,6 +311,7 @@
     thy
     |> Global_Theory.store_thm (binding, th)
     |-> Thm.add_arity
+    |> put_arity_thyname (t, c)
     |> fold (#2 oo declare_overloaded) missing_params
   end;
 

--- a/src/Pure/thm.ML	Mon Aug 05 11:20:56 2019 +0200
+++ b/src/Pure/thm.ML	Mon Aug 05 16:11:43 2019 +0200
@@ -167,7 +167,6 @@
   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 add_classrel: thm -> theory -> theory
   val add_arity: thm -> theory -> theory
 end;
@@ -875,7 +874,7 @@
 
 datatype classes = Classes of
  {classrels: thm Symreltab.table,
-  arities: (thm * string * serial) Aritytab.table};
+  arities: thm Aritytab.table};
 
 fun make_classes (classrels, arities) = Classes {classrels = classrels, arities = arities};
 
@@ -928,7 +927,7 @@
 
 fun the_arity thy (a, Ss, c) =
   (case Aritytab.lookup (get_arities thy) (a, Ss, c) of
-    SOME (thm, _, _) => transfer thy thm
+    SOME thm => transfer thy thm
   | NONE => error ("Unproven type arity " ^
       Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));
 
@@ -2210,12 +2209,7 @@
 
 (* type arities *)
 
-fun thynames_of_arity thy (a, c) =
-  (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;
-
-fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) =
+fun insert_arity_completions thy ((t, Ss, c), th) (finished, arities) =
   let
     val completions =
       Sign.super_classes thy c |> map_filter (fn c1 =>
@@ -2227,7 +2221,7 @@
               |> standard_tvars
               |> close_derivation
               |> trim_context;
-          in SOME ((t, Ss, c1), (th1, thy_name, ser)) end);
+          in SOME ((t, Ss, c1), th1) end);
     val finished' = finished andalso null completions;
     val arities' = fold Aritytab.update completions arities;
   in (finished', arities') end;
@@ -2268,7 +2262,7 @@
     val th = strip_shyps (transfer thy raw_th);
     val prop = plain_prop_of th;
     val (t, Ss, c) = Logic.dest_arity prop;
-    val ar = ((t, Ss, c), (th |> unconstrainT |> trim_context, Context.theory_name thy, serial ()));
+    val ar = ((t, Ss, c), (th |> unconstrainT |> trim_context));
   in
     thy
     |> Sign.primitive_arity (t, Ss, [c])

--- a/src/Tools/Code/code_symbol.ML	Mon Aug 05 11:20:56 2019 +0200
+++ b/src/Tools/Code/code_symbol.ML	Mon Aug 05 16:11:43 2019 +0200
@@ -99,9 +99,9 @@
 local
   fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
   fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
-  fun thyname_of_instance thy inst = case Thm.thynames_of_arity thy inst
-   of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^  snd inst))
-    | thyname :: _ => thyname;
+  fun thyname_of_instance thy inst = case Axclass.get_arity_thyname thy inst
+   of NONE => error ("No such instance: " ^ quote (fst inst ^ " :: " ^  snd inst))
+    | SOME thyname => thyname;
   fun thyname_of_const thy c = case Axclass.class_of_param thy c
    of SOME class => thyname_of_class thy class
     | NONE => (case Code.get_type_of_constr_or_abstr thy c