src/Pure/Isar/class_declaration.ML
changeset 58319 9228350683d0
parent 58294 7f990b3d5189
child 58837 e84d900cd287
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Sep 11 21:11:03 2014 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Sep 11 18:33:56 2014 +0200
     1.3 @@ -146,14 +146,14 @@
     1.4        let
     1.5          val param_Ts = (fold o fold_aterms)
     1.6            (fn Free (v, T) => if is_param v then fold_atyps (insert (op =)) T else I | _ => I) ts [];
     1.7 -        val param_Ts_subst = map_filter (try dest_TVar) param_Ts;
     1.8 -        val param_T = if null param_Ts_subst then NONE
     1.9 +        val param_namesT = map_filter (try (fst o dest_TVar)) param_Ts;
    1.10 +        val param_T = if null param_namesT then NONE
    1.11            else SOME (case get_first (try dest_TFree) param_Ts of
    1.12              SOME v_sort => TFree v_sort |
    1.13 -            NONE => TVar ((fst o hd) param_Ts_subst, fold (inter_sort o snd) param_Ts_subst []));
    1.14 +            NONE => TVar (hd param_namesT, proto_base_sort));
    1.15        in case param_T of
    1.16          NONE => ts |
    1.17 -        SOME T => map (subst_TVars (map (rpair T o fst) param_Ts_subst)) ts
    1.18 +        SOME T => map (subst_TVars (map (rpair T) param_namesT)) ts
    1.19        end;
    1.20  
    1.21      (* preprocessing elements, retrieving base sort from type-checked elements *)