src/Pure/Isar/class_declaration.ML
changeset 38875 c7a66b584147
parent 38756 d07959fabde6
child 40188 eddda8e38360
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Mon Aug 30 15:09:20 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Mon Aug 30 15:19:39 2010 +0200
     1.3 @@ -126,8 +126,8 @@
     1.4                  else error ("Type inference imposes additional sort constraint "
     1.5                    ^ Syntax.string_of_sort_global thy inferred_sort
     1.6                    ^ " of type parameter " ^ Name.aT ^ " of sort "
     1.7 -                  ^ Syntax.string_of_sort_global thy a_sort ^ ".")
     1.8 -            | _ => error "Multiple type variables in class specification.";
     1.9 +                  ^ Syntax.string_of_sort_global thy a_sort)
    1.10 +            | _ => error "Multiple type variables in class specification";
    1.11        in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
    1.12      val after_infer_fixate = (map o map_atyps)
    1.13        (fn T as TFree _ => T | T as TVar (vi, sort) =>