src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 20 11:42:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 20 13:32:48 2012 +0200
@@ -81,6 +81,7 @@
     no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
+    (* TODO: integration with function package ("size") *)
 
     val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
       else ();