src/Pure/Isar/class_declaration.ML
changeset 40188 eddda8e38360
parent 38875 c7a66b584147
child 41585 45d7da4e4ccf
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Tue Oct 26 13:50:18 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Tue Oct 26 14:06:22 2010 +0200
     1.3 @@ -129,9 +129,15 @@
     1.4                    ^ Syntax.string_of_sort_global thy a_sort)
     1.5              | _ => error "Multiple type variables in class specification";
     1.6        in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
     1.7 -    val after_infer_fixate = (map o map_atyps)
     1.8 -      (fn T as TFree _ => T | T as TVar (vi, sort) =>
     1.9 -        if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort) else T);
    1.10 +    fun after_infer_fixate Ts =
    1.11 +      let
    1.12 +        val sort' = (fold o fold_atyps) (fn T as TFree _ => I | T as TVar (vi, sort) =>
    1.13 +          if Type_Infer.is_param vi then inter_sort sort else I) Ts [];
    1.14 +      in
    1.15 +        (map o map_atyps)
    1.16 +          (fn T as TFree _ => T | T as TVar (vi, _) =>
    1.17 +            if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts
    1.18 +      end;
    1.19      fun add_typ_check level name f = Context.proof_map
    1.20        (Syntax.add_typ_check level name (fn Ts => fn ctxt =>
    1.21          let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));