--- a/src/HOL/BNF_LFP.thy Mon Aug 18 19:16:51 2014 +0200
+++ b/src/HOL/BNF_LFP.thy Mon Aug 18 19:18:08 2014 +0200
@@ -193,8 +193,6 @@
ML_file "Tools/BNF/bnf_lfp_compat.ML"
ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
-datatype_new 'a l = N | C 'a "'a l"
-
hide_fact (open) id_transfer
end