diff -r b7bc5ba2f3fb -r 8ee2d984caa8 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:38:13 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:38:40 2014 +0200
@@ -47,7 +47,7 @@
    xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
    xtor_co_rec_o_maps = [ctor_rec_o_map],
    xtor_rel_co_induct = xtor_rel_induct,
-   dtor_set_induct_thms = [],
+   dtor_set_inducts = [],
    xtor_co_rec_transfer_thms = []};
 
 fun fp_sugar_of_sum ctxt =