--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Jul 30 10:50:28 2014 +0200
@@ -463,7 +463,8 @@
xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
xtor_co_rec_thms = xtor_co_rec_thms,
xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
- rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
+ rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
+ dtor_set_induct_thms = []}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
(fp_res, lthy)