diff -r ec53c138277a -r ee83040c3c84 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Wed Mar 08 10:19:57 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Wed Mar 08 16:29:07 2006 +0100
@@ -35,9 +35,9 @@
   val the_superclasses: theory -> class -> class list
   val the_consts_sign: theory -> class -> string * (string * typ) list
   val lookup_const_class: theory -> string -> class option
-  val the_instances: theory -> class -> (string * string) list
+  val the_instances: theory -> class -> (string * ((sort list) * string)) list
   val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
-  val get_classtab: theory -> (string list * (string * string) list) Symtab.table
+  val get_classtab: theory -> (string * string) list Symtab.table
 
   val print_classes: theory -> unit
   val intro_classes_tac: thm list -> tactic
@@ -62,23 +62,25 @@
   name_axclass: string,
   intro: thm option,
   var: string,
-  consts: (string * typ) list,
-  insts: (string * string) list (* [type constructor ~> theory name] *)
+  consts: (string * typ) list
 };
 
 structure ClassData = TheoryDataFun (
   struct
     val name = "Pure/classes";
-    type T = class_data Graph.T * (class Symtab.table * string Symtab.table);
-    val empty = (Graph.empty, (Symtab.empty, Symtab.empty));
+    type T = (class_data Graph.T
+      * (string * (sort list * string)) list Symtab.table)
+        (* class ~> tyco ~> (arity, thyname) *)
+      * class Symtab.table;
+    val empty = ((Graph.empty, Symtab.empty), Symtab.empty);
     val copy = I;
     val extend = I;
-    fun merge _ ((t1, (c1, l1)), (t2, (c2, l2)))=
-      (Graph.merge (op =) (t1, t2),
-       (Symtab.merge (op =) (c1, c2), Symtab.merge (op =) (l1, l2)));
-    fun print thy (gr, _) =
+    fun merge _ (((g1, c1), f1), ((g2, c2), f2)) =
+      ((Graph.merge (op =) (g1, g2), Symtab.join (fn _ => AList.merge (op =) (K false)) (c1, c2)),
+       Symtab.merge (op =) (f1, f2));
+    fun print thy ((gr, _), _) =
       let
-        fun pretty_class gr (name, {name_locale, name_axclass, intro, var, consts, insts}) =
+        fun pretty_class gr (name, {name_locale, name_axclass, intro, var, consts}) =
           (Pretty.block o Pretty.fbreaks) [
             Pretty.str ("class " ^ name ^ ":"),
             (Pretty.block o Pretty.fbreaks) (
@@ -91,10 +93,6 @@
             (Pretty.block o Pretty.fbreaks) (
               Pretty.str "constants: "
               :: map (fn (c, ty) => Pretty.str (c ^ " :: " ^ Sign.string_of_typ thy ty)) consts
-            ),
-            (Pretty.block o Pretty.fbreaks) (
-              Pretty.str "instances: "
-              :: map (fn (tyco, thyname) => Pretty.str (tyco ^ ", in theory " ^ thyname)) insts
             )
           ]
       in
@@ -110,9 +108,9 @@
 
 (* queries *)
 
-val lookup_class_data = try o Graph.get_node o fst o ClassData.get;
-val lookup_const_class = Symtab.lookup o fst o snd o ClassData.get;
-val lookup_locale_class = Symtab.lookup o snd o snd o ClassData.get;
+val lookup_class_data = try o Graph.get_node o fst o fst o ClassData.get;
+val the_instances = these oo Symtab.lookup o snd o fst o ClassData.get;
+val lookup_const_class = Symtab.lookup o snd o ClassData.get;
 
 fun the_class_data thy class =
   case lookup_class_data thy class
@@ -148,7 +146,7 @@
 fun get_superclass_derivation thy (subclass, superclass) =
   if subclass = superclass
     then SOME [subclass]
-    else case Graph.find_paths ((fst o ClassData.get) thy) (subclass, superclass)
+    else case Graph.find_paths ((fst o fst o ClassData.get) thy) (subclass, superclass)
       of [] => NONE
        | (p::_) => (SOME o filter (is_class thy)) p;
 
@@ -162,7 +160,7 @@
 
 fun the_intros thy =
   let
-    val gr = (fst o ClassData.get) thy;
+    val gr = (fst o fst o ClassData.get) thy;
   in (List.mapPartial (#intro o Graph.get_node gr) o Graph.keys) gr end;
 
 fun subst_clsvar v ty_subst =
@@ -174,15 +172,11 @@
     val data = the_class_data thy class
   in (#var data, #consts data) end;
 
-val the_instances =
-  #insts oo the_class_data;
-
 fun the_inst_sign thy (class, tyco) =
   let
     val _ = if is_class thy class then () else error ("no syntactic class: " ^ class);
     val arity =
-      Sorts.mg_domain (Sign.classes_arities_of thy) tyco [class]
-      |> map (operational_sort_of thy);
+      (fst o the o AList.lookup (op =) (the_instances thy class)) tyco
     val clsvar = (#var o the_class_data thy) class;
     val const_sign = (snd o the_consts_sign thy) class;
     fun add_var sort used =
@@ -190,7 +184,7 @@
         val v = hd (Term.invent_names used "'a" 1)
       in ((v, sort), v::used) end;
     val (vsorts, _) =
-      []
+      [clsvar]
       |> fold (fn (_, ty) => curry (gen_union (op =))
            ((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign
       |> fold_map add_var arity;
@@ -199,43 +193,33 @@
   in (vsorts, inst_signs) end;
 
 fun get_classtab thy =
-  Graph.fold_nodes
-    (fn (class, { consts = consts, insts = insts, ... }) =>
-      Symtab.update_new (class, (map fst consts, insts)))
-       ((fst o ClassData.get) thy) Symtab.empty;
+  (Symtab.map o map)
+    (fn (tyco, (_, thyname)) => (tyco, thyname)) ((snd o fst o ClassData.get) thy);
 
 
 (* updaters *)
 
 fun add_class_data (class, (superclasses, name_locale, name_axclass, intro, var, consts)) =
-  ClassData.map (fn (classtab, (consttab, loctab)) => (
-    classtab
+  ClassData.map (fn ((gr, tab), consttab) => ((
+    gr
     |> Graph.new_node (class, {
          name_locale = name_locale,
          name_axclass = name_axclass,
          intro = intro,
          var = var,
-         consts = consts,
-         insts = []
+         consts = consts
        })
     |> fold (curry Graph.add_edge_acyclic class) superclasses,
-    (consttab
-    |> fold (fn (c, _) => Symtab.update (c, class)) consts,
-    loctab
-    |> Symtab.update (name_locale, class))
+    tab
+    |> Symtab.update (class, [])),
+    consttab
+    |> fold (fn (c, _) => Symtab.update (c, class)) consts
   ));
 
 fun add_inst_data (class, inst) =
-  (ClassData.map o apfst o Graph.map_node class)
-    (fn {name_locale, name_axclass, intro, var, consts, insts}
-      => {
-           name_locale = name_locale,
-           name_axclass = name_axclass,
-           intro = intro,
-           var = var,
-           consts = consts,
-           insts = insts @ [inst]
-          });
+  ClassData.map (fn ((gr, tab), consttab) =>
+     ((gr, tab |>
+    (Symtab.map_entry class (AList.update (op =) inst))), consttab));
 
 
 (* name handling *)
@@ -468,7 +452,7 @@
     fun get_classes thy tyco sort =
       let
         fun get class classes =
-          if AList.defined (op =) ((#insts o the_class_data thy) class) tyco
+          if AList.defined (op =) ((the_instances thy) class) tyco
             then classes
             else classes
               |> cons class
@@ -524,7 +508,7 @@
     fun after_qed cs thy =
       thy
       |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
-      |> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort;
+      |> fold (fn class => add_inst_data (class, (tyco, (asorts, Context.theory_name thy)))) sort;
   in
     theory
     |> check_defs raw_defs cs
@@ -623,7 +607,16 @@
   |> filter (not o null o snd);
 
 datatype classlookup = Instance of (class * string) * classlookup list list
-                    | Lookup of class list * (string * int)
+                     | Lookup of class list * (string * int)
+
+fun pretty_lookup' (Instance ((class, tyco), lss)) =
+      (Pretty.block o Pretty.breaks) (
+        Pretty.enum "," "{" "}" [Pretty.str class, Pretty.str tyco]
+        :: map pretty_lookup lss
+      )
+  | pretty_lookup' (Lookup (classes, (v, i))) =
+      Pretty.enum " <" "[" "]" (map Pretty.str classes @ [Pretty.str (v ^ "!" ^ string_of_int i)])
+and pretty_lookup ls = (Pretty.enum "," "(" ")" o map pretty_lookup') ls;
 
 fun extract_lookup thy sortctxt raw_typ_def raw_typ_use =
   let
@@ -646,11 +639,12 @@
           ) subclasses;
         val i' = if length subclasses = 1 then ~1 else i;
       in (rev deriv, i') end;
-    fun mk_lookup (sort_def, (Type (tycon, tys))) =
-          let
-            val arity_lookup = map2 (curry mk_lookup)
-              (map (operational_sort_of thy) (Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort_def)) tys
-          in map (fn class => Instance ((class, tycon), arity_lookup)) sort_def end
+    fun mk_lookup (sort_def, (Type (tyco, tys))) =
+          map (fn class => Instance ((class, tyco),
+            map2 (curry mk_lookup)
+              ((fst o the o AList.lookup (op =) (the_instances thy class)) tyco)
+              tys)
+          ) sort_def
       | mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
           let
             fun mk_look class =
@@ -659,15 +653,10 @@
           in map mk_look sort_def end;
   in
     sortctxt
-(*     |> print  *)
     |> map (tab_lookup o fst)
-(*     |> print  *)
     |> map (apfst (operational_sort_of thy))
-(*     |> print  *)
     |> filter (not o null o fst)
-(*     |> print  *)
     |> map mk_lookup
-(*     |> print  *)
   end;
 
 fun extract_classlookup thy (c, raw_typ_use) =