# HG changeset patch
# User haftmann
# Date 1410453236 -7200
# Node ID 9228350683d05499af0243ea25249f84bf5fc3b6
# Parent  f95754ca70825a8f3ce0e6e7f2f8e34aa6596987
use proto_base_sort uniformly

diff -r f95754ca7082 -r 9228350683d0 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Thu Sep 11 21:11:03 2014 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Thu Sep 11 18:33:56 2014 +0200
@@ -146,14 +146,14 @@
       let
         val param_Ts = (fold o fold_aterms)
           (fn Free (v, T) => if is_param v then fold_atyps (insert (op =)) T else I | _ => I) ts [];
-        val param_Ts_subst = map_filter (try dest_TVar) param_Ts;
-        val param_T = if null param_Ts_subst then NONE
+        val param_namesT = map_filter (try (fst o dest_TVar)) param_Ts;
+        val param_T = if null param_namesT then NONE
           else SOME (case get_first (try dest_TFree) param_Ts of
             SOME v_sort => TFree v_sort |
-            NONE => TVar ((fst o hd) param_Ts_subst, fold (inter_sort o snd) param_Ts_subst []));
+            NONE => TVar (hd param_namesT, proto_base_sort));
       in case param_T of
         NONE => ts |
-        SOME T => map (subst_TVars (map (rpair T o fst) param_Ts_subst)) ts
+        SOME T => map (subst_TVars (map (rpair T) param_namesT)) ts
       end;
 
     (* preprocessing elements, retrieving base sort from type-checked elements *)