src/HOL/Tools/BNF/bnf_gfp.ML
changeset 58448 a1d4e7473c98
parent 58446 e89f57d1e46c
child 58578 9ff8ca957c02
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 16:35:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 16:35:56 2014 +0200
@@ -2542,7 +2542,8 @@
        xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
        xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
        xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
-       dtor_set_induct_thms = dtor_Jset_induct_thms, ctor_rec_transfer_thms = []};
+       dtor_set_induct_thms = dtor_Jset_induct_thms,
+       xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
   in
     timer; (fp_res, lthy')
   end;