src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
changeset 58579 b7bc5ba2f3fb
parent 58578 9ff8ca957c02
child 58580 8ee2d984caa8
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:37:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:38:13 2014 +0200
@@ -46,7 +46,7 @@
    xtor_rel_thms = [xtor_rel],
    xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
    xtor_co_rec_o_maps = [ctor_rec_o_map],
-   rel_xtor_co_induct_thm = xtor_rel_induct,
+   xtor_rel_co_induct = xtor_rel_induct,
    dtor_set_induct_thms = [],
    xtor_co_rec_transfer_thms = []};