# HG changeset patch
# User wenzelm
# Date 1086800128 -7200
# Node ID 2da524f3d785ecabb6eeed019b9678db2829a1c8
# Parent  5f3fc2f620711edca8e8e764011fec22a990f6da
tuned messages;

diff -r 5f3fc2f62071 -r 2da524f3d785 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Jun 09 18:55:07 2004 +0200
+++ b/src/Pure/type.ML	Wed Jun 09 18:55:28 2004 +0200
@@ -547,12 +547,8 @@
   error ("Negative number of arguments in type constructor declaration: " ^ quote c);
 
 fun err_in_decls c decl decl' =
-  let
-    val s = str_of_decl decl;
-    val s' = str_of_decl decl';
-  in
-    if s = s' then
-      error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
+  let val s = str_of_decl decl and s' = str_of_decl decl' in
+    if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
     else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
   end;
 
@@ -569,7 +565,7 @@
 fun add_abbr (a, vs, rhs) tsig = tsig |> change_types (fn types =>
   let
     fun err msg =
-      error (msg ^ "\nThe error(s) above occurred in type abbreviation " ^ quote a);
+      error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
     val rhs' = strip_sorts (varifyT (no_tvars (cert_typ_syntax tsig rhs)))
       handle TYPE (msg, _, _) => err msg;
   in