# HG changeset patch
# User blanchet
# Date 1307426244 -7200
# Node ID 359c190ede756284a171ccadcb4285c3b65eed40
# Parent  a4a314a0a90a00f9d9f01b5512fa9dbe76616cc8
fixed typo in legacy feature message

diff -r a4a314a0a90a -r 359c190ede75 src/Pure/Isar/isar_syn.ML
--- 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 _ =