src/HOL/BNF/Tools/bnf_lfp.ML

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Oct 02 10:39:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Oct 02 10:53:15 2013 +0200
@@ -1884,7 +1884,7 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes"
+  Outer_Syntax.local_theory @{command_spec "datatype_new"} "define new-style inductive datatypes"
     (parse_co_datatype_cmd Least_FP construct_lfp);
 
 val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"}