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