note exhaust proof obligation

--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Dec 20 09:48:04 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Dec 20 11:12:51 2013 +0100
@@ -1141,6 +1141,7 @@
            (codeN, code_thmss, code_nitpicksimp_attrs),
            (ctrN, ctr_thmss, []),
            (discN, disc_thmss, simp_attrs),
+           (exhaustN, map the_list maybe_exhaust_thms, []),
            (selN, sel_thmss, simp_attrs),
            (simpsN, simp_thmss, []),
            (strong_coinductN, map (if n2m then single else K []) strong_coinduct_thms, [])]