# HG changeset patch
# User blanchet
# Date 1347291362 -7200
# Node ID e9cdacf44cc3d809662d8285dea752caa548390b
# Parent  df98aeb80a19a151a6cb927879a2ca70fce3edb5
removed done TODO

diff -r df98aeb80a19 -r e9cdacf44cc3 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 10 17:36:02 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 10 17:36:02 2012 +0200
@@ -196,7 +196,6 @@
     val missing_alternate_disc_def = FalseE; (*arbitrary marker*)
 
     (* TODO: Allow use of same selector for several constructors *)
-    (* TODO: Allow use of same name for datatype and for constructor, e.g. "data L = L" *)
 
     val (((raw_discs, raw_disc_defs), (raw_selss, raw_sel_defss)), (lthy', lthy)) =
       no_defs_lthy