tuned messages;
authorwenzelm
Wed Jun 09 18:55:28 2004 +0200 (2004-06-09 ago)
changeset 149062da524f3d785
parent 14905 5f3fc2f62071
child 14907 c77fda9b6cf0
tuned messages;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Wed Jun 09 18:55:07 2004 +0200
     1.2 +++ b/src/Pure/type.ML	Wed Jun 09 18:55:28 2004 +0200
     1.3 @@ -547,12 +547,8 @@
     1.4    error ("Negative number of arguments in type constructor declaration: " ^ quote c);
     1.5  
     1.6  fun err_in_decls c decl decl' =
     1.7 -  let
     1.8 -    val s = str_of_decl decl;
     1.9 -    val s' = str_of_decl decl';
    1.10 -  in
    1.11 -    if s = s' then
    1.12 -      error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
    1.13 +  let val s = str_of_decl decl and s' = str_of_decl decl' in
    1.14 +    if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
    1.15      else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
    1.16    end;
    1.17  
    1.18 @@ -569,7 +565,7 @@
    1.19  fun add_abbr (a, vs, rhs) tsig = tsig |> change_types (fn types =>
    1.20    let
    1.21      fun err msg =
    1.22 -      error (msg ^ "\nThe error(s) above occurred in type abbreviation " ^ quote a);
    1.23 +      error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
    1.24      val rhs' = strip_sorts (varifyT (no_tvars (cert_typ_syntax tsig rhs)))
    1.25        handle TYPE (msg, _, _) => err msg;
    1.26    in