# HG changeset patch
# User wenzelm
# Date 1010076975 -3600
# Node ID 9ed65232429c4e5d79cebbc9ef8d3d1c9a28d9ab
# Parent  7a33541fd81bee67a23a67d6c4f0e981c910b769
tuned msg;

diff -r 7a33541fd81b -r 9ed65232429c src/HOL/Tools/typedef_package.ML
--- 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)])));
 
diff -r 7a33541fd81b -r 9ed65232429c src/Pure/Isar/isar_syn.ML
--- 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))));
 
diff -r 7a33541fd81b -r 9ed65232429c src/Pure/Thy/thy_parse.ML
--- 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;