1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 20:23:08 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 23:54:54 2013 +0200
     1.3 @@ -827,6 +827,10 @@
     1.4                |> single
     1.5            end;
     1.6  
     1.7 +        (* TODO: please reorganize so that the list looks like elsewhere in the BNF code.
     1.8 +           This is important because we continually add new theorems, change attributes, etc., and
     1.9 +           need to have a clear overview (and keep the documentation in sync). Also, it's confusing
    1.10 +           that some variables called '_thmss' are actually pairs. *)
    1.11          val (disc_notes, disc_thmss) =
    1.12            fun_names ~~ map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss
    1.13            |> `(map (fn (fun_name, thms) =>