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 = []};