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