tuned msg;

--- a/src/HOL/Tools/typedef_package.ML	Thu Jan 03 17:55:46 2002 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Thu Jan 03 17:56:15 2002 +0100
@@ -261,7 +261,7 @@
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
 val typedeclP =
-  OuterSyntax.command "typedecl" "HOL type declaration" K.thy_decl
+  OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
     (P.type_args -- P.name -- P.opt_infix --| P.marg_comment >> (fn ((vs, t), mx) =>
       Toplevel.theory (add_typedecls [(t, vs, mx)])));
 

--- a/src/Pure/Isar/isar_syn.ML	Thu Jan 03 17:55:46 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jan 03 17:56:15 2002 +0100
@@ -102,7 +102,7 @@
 (* types *)
 
 val typedeclP =
-  OuterSyntax.command "typedecl" "Pure type declaration" K.thy_decl
+  OuterSyntax.command "typedecl" "type declaration" K.thy_decl
     (P.type_args -- P.name -- P.opt_infix -- P.marg_comment >> (fn (((args, a), mx), cmt) =>
       Toplevel.theory (IsarThy.add_typedecl ((a, args, mx), cmt))));
 

--- a/src/Pure/Thy/thy_parse.ML	Thu Jan 03 17:55:46 2002 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Thu Jan 03 17:56:15 2002 +0100
@@ -446,7 +446,7 @@
     val keys = map Symbol.explode (map fst sects' @ keywords);
   in
     if null dups then ()
-    else warning ("Duplicate declaration of theory file sections:\n" ^ commas_quote dups);
+    else warning ("Duplicate declaration of theory file section(s): " ^ commas_quote dups);
     (Scan.make_lexicon keys, Symtab.make sects')
   end;