# HG changeset patch
# User blanchet
# Date 1346756548 -7200
# Node ID ef3eea7ae251a7d5684c73b3b2cd8a6ba44650f2
# Parent  4de4635d8f93430133464342c301b5710c53e9cc
tuned TODOs

diff -r 4de4635d8f93 -r ef3eea7ae251 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:28 2012 +0200
@@ -64,8 +64,10 @@
   no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
-
-    (* TODO: normalize types of constructors w.r.t. each other *)
+    (* 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;
@@ -379,9 +381,6 @@
             (split_thm, split_asm_thm)
           end;
 
-        (* TODO: case syntax *)
-        (* TODO: attributes (simp, case_names, etc.) *)
-
         val notes =
           [(case_congN, [case_cong_thm]),
            (case_discsN, [case_disc_thm]),