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