tuned;
authorwenzelm
Tue May 16 13:01:31 2006 +0200 (2006-05-16)
changeset 19648702843484da6
parent 19647 043921b0e587
child 19649 c887656778bc
tuned;
src/Pure/Tools/class_package.ML
     1.1 --- a/src/Pure/Tools/class_package.ML	Tue May 16 13:01:30 2006 +0200
     1.2 +++ b/src/Pure/Tools/class_package.ML	Tue May 16 13:01:31 2006 +0200
     1.3 @@ -70,15 +70,6 @@
     1.4  };
     1.5  
     1.6  fun rep_classdata (ClassData c) = c;
     1.7 -fun eq_classdata (ClassData {
     1.8 -  name_locale = name_locale1, name_axclass = name_axclass1, intro = intro1,
     1.9 -    var = var1, consts = consts1}, ClassData {
    1.10 -  name_locale = name_locale2, name_axclass = name_axclass2, intro = intro2,
    1.11 -    var = var2, consts = consts2}) =
    1.12 -  name_locale1 = name_locale2 andalso name_axclass1 = name_axclass2
    1.13 -  andalso eq_opt eq_thm (intro1, intro2) andalso var1 = var2
    1.14 -  andalso eq_list (eq_pair (op =) (eq_pair (op =) (Type.eq_type Vartab.empty)))
    1.15 -    (consts1, consts2);
    1.16  
    1.17  structure ClassData = TheoryDataFun (
    1.18    struct
    1.19 @@ -91,7 +82,7 @@
    1.20      val copy = I;
    1.21      val extend = I;
    1.22      fun merge _ (((g1, c1), f1) : T, ((g2, c2), f2)) =
    1.23 -      ((Graph.merge eq_classdata (g1, g2), Symtab.join (fn _ => AList.merge (op =) (op =)) (c1, c2)),
    1.24 +      ((Graph.merge (K true) (g1, g2), Symtab.join (fn _ => AList.merge (op =) (op =)) (c1, c2)),
    1.25         Symtab.merge (op =) (f1, f2));
    1.26      fun print thy ((gr, _), _) =
    1.27        let