# 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