# HG changeset patch
# User haftmann
# Date 1288098057 -7200
# Node ID 2c77c2e5788742d889196b81d5f15c1d60e16041
# Parent  9b6e918682d577215bfd9476534699aff4c9aab6# Parent  eddda8e38360b6ba342a07064b9f7090c777fe5c
merged

diff -r 9b6e918682d5 -r 2c77c2e57887 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Tue Oct 26 15:00:42 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Tue Oct 26 15:00:57 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));