# HG changeset patch # User blanchet # Date 1379627694 -7200 # Node ID 87585d506db4ec7870bbeadc3c0ed885ee25c932 # Parent 30f4b24b3e8aeeea414257db7307f49e53bf5b49 added TODO diff -r 30f4b24b3e8a -r 87585d506db4 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- 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) =>