proper merge of base sorts
authorhaftmann
Wed Feb 27 21:41:05 2008 +0100 (2008-02-27)
changeset 26167ccc9007a7164
parent 26166 dbeab703a28d
child 26168 3bd9ac4e0b97
proper merge of base sorts
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Wed Feb 27 18:01:10 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Feb 27 21:41:05 2008 +0100
     1.3 @@ -521,7 +521,8 @@
     1.4      val supsort = Sign.minimize_sort thy supclasses;
     1.5      val sups = filter (is_class thy) supsort;
     1.6      val base_sort = if null sups then supsort else
     1.7 -      (#base_sort o the_class_data thy o hd) sups;
     1.8 +      foldr1 (Sorts.inter_sort (Sign.classes_of thy))
     1.9 +        (map (#base_sort o the_class_data thy) sups);
    1.10      val suplocales = map Locale.Locale sups;
    1.11      val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
    1.12        | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
    1.13 @@ -529,7 +530,7 @@
    1.14      val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
    1.15      val mergeexpr = Locale.Merge (suplocales @ includes);
    1.16      val constrain = Element.Constrains ((map o apsnd o map_atyps)
    1.17 -      (fn TFree (_, sort) => TFree (Name.aT, sort)) supparams);
    1.18 +      (K (TFree (Name.aT, base_sort))) supparams);
    1.19      fun fork_syn (Element.Fixes xs) =
    1.20            fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
    1.21            #>> Element.Fixes