src/HOL/BNF/Tools/bnf_gfp.ML

     val surj_ctor_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_ctor_thms;
     val ctor_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_ctor_thms;
     val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms;
     val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms;
 
-    fun mk_ctor_dtor_unfold_like_thm dtor_inject dtor_ctor unfold =
-      iffD1 OF [dtor_inject, trans OF [unfold, dtor_ctor RS sym]];
-
-    val ctor_dtor_unfold_thms =
-      map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_unfold_thms;
-
     val timer = time (timer "ctor definitions & thms");
 
     val corec_Inl_sum_thms =
       let
         val mor = mor_comp_thm OF [mor_sum_case_thm, mor_unfold_thm];

     val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
       `split_conj_thm (split_conj_prems n
         (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
         |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
            map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
-
-    val ctor_dtor_corec_thms =
-      map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms;
 
     val timer = time (timer "corec definitions & thms");
 
     val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) =
       let

         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
       val notes =
         [(ctor_dtorN, ctor_dtor_thms),
-        (ctor_dtor_corecN, ctor_dtor_corec_thms),
-        (ctor_dtor_unfoldN, ctor_dtor_unfold_thms),
         (ctor_exhaustN, ctor_exhaust_thms),
         (ctor_injectN, ctor_inject_thms),
         (dtor_corecN, dtor_corec_thms),
         (dtor_ctorN, dtor_ctor_thms),
         (dtor_exhaustN, dtor_exhaust_thms),

   in
     timer;
     ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors,
       xtor_co_iterss = transpose [unfolds, corecs],
       xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
-      ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
+      ctor_dtors = ctor_dtor_thms,
+      ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
       xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss',
       xtor_rel_thms = dtor_Jrel_thms,
-      xtor_co_iter_thmss = transpose [ctor_dtor_unfold_thms, ctor_dtor_corec_thms],
+      xtor_co_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms],
       xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_map_thms, dtor_corec_o_map_thms],
       rel_co_induct_thm = Jrel_coinduct_thm},
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;