# HG changeset patch
# User haftmann
# Date 1288094782 -7200
# Node ID eddda8e38360b6ba342a07064b9f7090c777fe5c
# Parent  0ea94d19af0835f9212d1dfba2cda1eab5ec1493
consider base sorts of superclasses simultaneously during processing of class specification -- avoids clash of different base sorts

diff -r 0ea94d19af08 -r eddda8e38360 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Tue Oct 26 13:50:18 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Tue Oct 26 14:06:22 2010 +0200
@@ -129,9 +129,15 @@
                   ^ Syntax.string_of_sort_global thy a_sort)
             | _ => error "Multiple type variables in class specification";
       in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
-    val after_infer_fixate = (map o map_atyps)
-      (fn T as TFree _ => T | T as TVar (vi, sort) =>
-        if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort) else T);
+    fun after_infer_fixate Ts =
+      let
+        val sort' = (fold o fold_atyps) (fn T as TFree _ => I | T as TVar (vi, sort) =>
+          if Type_Infer.is_param vi then inter_sort sort else I) Ts [];
+      in
+        (map o map_atyps)
+          (fn T as TFree _ => T | T as TVar (vi, _) =>
+            if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts
+      end;
     fun add_typ_check level name f = Context.proof_map
       (Syntax.add_typ_check level name (fn Ts => fn ctxt =>
         let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));