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