diff -r ed95293f14b6 -r 86b5b02ef33a src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 16:35:50 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 16:35:51 2014 +0200
@@ -2500,7 +2500,8 @@
     val dtor_corec_transfer_thms =
       mk_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
         (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs)
-        (fn {context = ctxt, prems = _} => print_tac ctxt "xxx" THEN Skip_Proof.cheat_tac 1)
+        (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs
+           dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms)
         lthy;
 
     val timer = time (timer "relator coinduction");
@@ -2517,6 +2518,7 @@
       (ctor_exhaustN, ctor_exhaust_thms),
       (ctor_injectN, ctor_inject_thms),
       (dtor_corecN, dtor_corec_thms),
+      (dtor_corec_transferN, dtor_corec_transfer_thms),
       (dtor_ctorN, dtor_ctor_thms),
       (dtor_exhaustN, dtor_exhaust_thms),
       (dtor_injectN, dtor_inject_thms),