tuned TODO comment
authorblanchet
Tue, 04 Sep 2012 13:02:30 +0200
changeset 49117 000deee4913e
parent 49116 3d520eec2746
child 49118 b815fa776b91
tuned TODO comment
src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:30 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:30 2012 +0200
@@ -68,7 +68,6 @@
     (* TODO: attributes (simp, case_names, etc.) *)
     (* TODO: case syntax *)
     (* TODO: integration with function package ("size") *)
-    (* TODO: omission of needless discriminators *)
 
     val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
     val caseof0 = prep_term no_defs_lthy raw_caseof;