src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
changeset 58578 9ff8ca957c02
parent 58577 15337ad05370
child 58579 b7bc5ba2f3fb
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:36:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:37:38 2014 +0200
@@ -45,7 +45,7 @@
    xtor_set_thmss = [xtor_sets],
    xtor_rel_thms = [xtor_rel],
    xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
-   xtor_co_rec_o_map_thms = [ctor_rec_o_map],
+   xtor_co_rec_o_maps = [ctor_rec_o_map],
    rel_xtor_co_induct_thm = xtor_rel_induct,
    dtor_set_induct_thms = [],
    xtor_co_rec_transfer_thms = []};