1.1 --- a/src/Pure/Tools/class_package.ML	Mon Apr 24 16:36:07 2006 +0200
     1.2 +++ b/src/Pure/Tools/class_package.ML	Mon Apr 24 16:36:34 2006 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4  
     1.5  (* theory data *)
     1.6  
     1.7 -type class_data = {
     1.8 +datatype class_data = ClassData of {
     1.9    name_locale: string,
    1.10    name_axclass: string,
    1.11    intro: thm option,
    1.12 @@ -69,22 +69,33 @@
    1.13      (*locale parameter ~> toplevel const*)
    1.14  };
    1.15  
    1.16 +fun rep_classdata (ClassData c) = c;
    1.17 +fun eq_classdata (ClassData {
    1.18 +  name_locale = name_locale1, name_axclass = name_axclass1, intro = intro1,
    1.19 +    var = var1, consts = consts1}, ClassData {
    1.20 +  name_locale = name_locale2, name_axclass = name_axclass2, intro = intro2,
    1.21 +    var = var2, consts = consts2}) =
    1.22 +  name_locale1 = name_locale2 andalso name_axclass1 = name_axclass2
    1.23 +  andalso eq_opt eq_thm (intro1, intro2) andalso var1 = var2
    1.24 +  andalso eq_list (eq_pair (op =) (eq_pair (op =) (Type.eq_type Vartab.empty)))
    1.25 +    (consts1, consts2);
    1.26 +
    1.27  structure ClassData = TheoryDataFun (
    1.28    struct
    1.29      val name = "Pure/classes";
    1.30      type T = (class_data Graph.T
    1.31        * (string * (sort list * string)) list Symtab.table)
    1.32 -        (* class ~> tyco ~> (arity, thyname) *)
    1.33 +        (*class ~> tyco ~> (arity, thyname)*)
    1.34        * class Symtab.table;
    1.35      val empty = ((Graph.empty, Symtab.empty), Symtab.empty);
    1.36      val copy = I;
    1.37      val extend = I;
    1.38 -    fun merge _ (((g1, c1), f1), ((g2, c2), f2)) =
    1.39 -      ((Graph.merge (op =) (g1, g2), Symtab.join (fn _ => AList.merge (op =) (op =)) (c1, c2)),
    1.40 +    fun merge _ (((g1, c1), f1) : T, ((g2, c2), f2)) =
    1.41 +      ((Graph.merge eq_classdata (g1, g2), Symtab.join (fn _ => AList.merge (op =) (op =)) (c1, c2)),
    1.42         Symtab.merge (op =) (f1, f2));
    1.43      fun print thy ((gr, _), _) =
    1.44        let
    1.45 -        fun pretty_class gr (name, {name_locale, name_axclass, intro, var, consts}) =
    1.46 +        fun pretty_class gr (name, ClassData {name_locale, name_axclass, intro, var, consts}) =
    1.47            (Pretty.block o Pretty.fbreaks) [
    1.48              Pretty.str ("class " ^ name ^ ":"),
    1.49              (Pretty.block o Pretty.fbreaks) (
    1.50 @@ -112,7 +123,7 @@
    1.51  
    1.52  (* queries *)
    1.53  
    1.54 -val lookup_class_data = try o Graph.get_node o fst o fst o ClassData.get;
    1.55 +val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o fst o ClassData.get;
    1.56  val the_instances = these oo Symtab.lookup o snd o fst o ClassData.get;
    1.57  val lookup_const_class = Symtab.lookup o snd o ClassData.get;
    1.58  
    1.59 @@ -166,7 +177,7 @@
    1.60  fun the_intros thy =
    1.61    let
    1.62      val gr = (fst o fst o ClassData.get) thy;
    1.63 -  in (List.mapPartial (#intro o Graph.get_node gr) o Graph.keys) gr end;
    1.64 +  in (List.mapPartial (#intro o rep_classdata o Graph.get_node gr) o Graph.keys) gr end;
    1.65  
    1.66  fun subst_clsvar v ty_subst =
    1.67    map_type_tfree (fn u as (w, _) =>
    1.68 @@ -214,7 +225,7 @@
    1.69  fun add_class_data (class, (superclasses, name_locale, name_axclass, intro, var, consts)) =
    1.70    ClassData.map (fn ((gr, tab), consttab) => ((
    1.71      gr
    1.72 -    |> Graph.new_node (class, {
    1.73 +    |> Graph.new_node (class, ClassData {
    1.74           name_locale = name_locale,
    1.75           name_axclass = name_axclass,
    1.76           intro = intro,