--- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Jul 30 10:50:28 2014 +0200
@@ -1814,7 +1814,8 @@
ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
- xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm}
+ xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
+ dtor_set_induct_thms = []}
|> morph_fp_result (substitute_noted_thm noted);
in
timer; (fp_res, lthy')