--- a/src/Pure/Isar/isar_syn.ML Tue Jun 07 07:45:12 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Jun 07 07:57:24 2011 +0200
@@ -119,7 +119,7 @@
val _ =
Outer_Syntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
(Scan.repeat1 type_abbrev >> (fn specs => fn lthy =>
- (legacy_feature "Old 'types' commands -- use 'type_synonym' instead";
+ (legacy_feature "Old 'types' command -- use 'type_synonym' instead";
fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs) specs lthy)));
val _ =