--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Apr 06 17:06:48 2015 +0200
@@ -788,7 +788,7 @@
>> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
val _ =
- Outer_Syntax.command @{command_spec "old_datatype"} "define old-style inductive datatypes"
+ Outer_Syntax.command @{command_keyword old_datatype} "define old-style inductive datatypes"
(Parse.and_list1 spec_cmd
>> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));