# HG changeset patch
# User haftmann
# Date 1204144865 -3600
# Node ID ccc9007a71647a3ed96e1be283756a30ba928e7c
# Parent  dbeab703a28d70d42e0f0aff4fb9a2b45d3688c0
proper merge of base sorts

diff -r dbeab703a28d -r ccc9007a7164 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Feb 27 18:01:10 2008 +0100
+++ b/src/Pure/Isar/class.ML	Wed Feb 27 21:41:05 2008 +0100
@@ -521,7 +521,8 @@
     val supsort = Sign.minimize_sort thy supclasses;
     val sups = filter (is_class thy) supsort;
     val base_sort = if null sups then supsort else
-      (#base_sort o the_class_data thy o hd) sups;
+      foldr1 (Sorts.inter_sort (Sign.classes_of thy))
+        (map (#base_sort o the_class_data thy) sups);
     val suplocales = map Locale.Locale sups;
     val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
       | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
@@ -529,7 +530,7 @@
     val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
     val mergeexpr = Locale.Merge (suplocales @ includes);
     val constrain = Element.Constrains ((map o apsnd o map_atyps)
-      (fn TFree (_, sort) => TFree (Name.aT, sort)) supparams);
+      (K (TFree (Name.aT, base_sort))) supparams);
     fun fork_syn (Element.Fixes xs) =
           fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
           #>> Element.Fixes