--- 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;