# HG changeset patch
# User blanchet
# Date 1408382288 -7200
# Node ID 45873fcbbf2ebd7636d9567b1a352aa9d0e2ebe3
# Parent  030ff4ceb6c3204c2a9bc28bd69ff034e2dcf2fb
removed junk

diff -r 030ff4ceb6c3 -r 45873fcbbf2e src/HOL/BNF_LFP.thy
--- 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