src/HOL/Tools/BNF/bnf_lfp.ML

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 11 18:54:36 2014 +0200
@@ -1814,6 +1814,10 @@
   end;
 
 val _ =
+  Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
+    (parse_co_datatype_cmd Least_FP construct_lfp);
+
+val _ =
   Outer_Syntax.local_theory @{command_spec "datatype_new"} "define inductive datatypes"
     (parse_co_datatype_cmd Least_FP construct_lfp);