# HG changeset patch
# User blanchet
# Date 1410457305 -7200
# Node ID ee1be8b3032e6270fda0233191f736f4b717d689
# Parent  57d2e5006d2989649b0b9cafa77b687ecf4370e4
compile

diff -r 57d2e5006d29 -r ee1be8b3032e src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 11 19:39:48 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 11 19:41:45 2014 +0200
@@ -13,7 +13,6 @@
 imports BNF_Fixpoint_Base
 keywords
   "datatype" :: thy_decl and
-  "datatype" :: thy_decl and
   "datatype_compat" :: thy_decl
 begin
 
diff -r 57d2e5006d29 -r ee1be8b3032e src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 11 19:39:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 11 19:41:45 2014 +0200
@@ -1817,10 +1817,6 @@
   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"} "define inductive datatypes"
-    (parse_co_datatype_cmd Least_FP construct_lfp);
-
 val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
 
 end;