src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML

             ([induct], fold_thmss, rec_thmss, [], [], [], []))
         else
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
             ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
-          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _,
-                  (disc_unfold_thmss, disc_corec_thmss, _),
+          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _,
+                  (disc_unfold_thmss, disc_corec_thmss, _), _,
                   (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
             (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
              disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));
 
       val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;