src/Pure/Isar/isar_syn.ML
changeset 12624 9ed65232429c
parent 12383 af14fd56b189
child 12696 f8dfc7845891
--- 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))));