src/HOL/Tools/BNF/bnf_lfp.ML
changeset 58578 9ff8ca957c02
parent 58448 a1d4e7473c98
child 58579 b7bc5ba2f3fb
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:36:48 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:37:38 2014 +0200
     1.3 @@ -1828,7 +1828,7 @@
     1.4         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
     1.5         xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
     1.6         xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
     1.7 -       xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
     1.8 +       xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
     1.9         dtor_set_induct_thms = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
    1.10    in
    1.11      timer; (fp_res, lthy')