# HG changeset patch
# User blanchet
# Date 1410210564 -7200
# Node ID 3fb224b61995b7fb21919d1ceb8942eb8a2e90e2
# Parent  ff8059e3e803f8b84f631b7c810aa7eb007b4bbe
tuned command descriptions

diff -r ff8059e3e803 -r 3fb224b61995 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Sep 08 23:09:23 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Sep 08 23:09:24 2014 +0200
@@ -1814,7 +1814,7 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "datatype_new"} "define new-style inductive datatypes"
+  Outer_Syntax.local_theory @{command_spec "datatype_new"} "define inductive datatypes"
     (parse_co_datatype_cmd Least_FP construct_lfp);
 
 end;
diff -r ff8059e3e803 -r 3fb224b61995 src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Sep 08 23:09:23 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Sep 08 23:09:24 2014 +0200
@@ -791,7 +791,7 @@
   >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
 
 val _ =
-  Outer_Syntax.command @{command_spec "datatype"} "define inductive datatypes"
+  Outer_Syntax.command @{command_spec "datatype"} "define old-style inductive datatypes"
     (Parse.and_list1 spec_cmd
       >> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));