src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

             val iter_T = flat g_Tss ---> fp_T --> C;
 
             val ((gss, ysss), _) =
               lthy
               |> mk_Freess "f" g_Tss
-              ||>> apfst (unflat y_Tsss) o mk_Freess "x" (flat y_Tsss);
+              ||>> mk_Freesss "x" y_Tsss;
 
             val iter_rhs =
               fold_rev (fold_rev Term.lambda) gss
                 (Term.list_comb (fp_iter, map2 (mk_sum_caseN oo map2 mk_uncurried_fun) gss ysss));
           in