src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

   in project end;
 
 val project_recT = project_co_recT @{type_name prod};
 val project_corecT = project_co_recT @{type_name sum};
 
-fun unzip_recT fpTs = meta_unzip_rec I (project_recT fpTs fst) (project_recT fpTs snd) I fpTs;
+fun unzip_recT fpTs (T as Type (@{type_name prod}, Ts as [T', _])) =
+    if member (op =) fpTs T' then Ts else [T]
+  | unzip_recT _ T = [T];
 
 fun mk_fun_arg_typess n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
 
 fun mk_iter_fun_arg_typessss fpTs ns mss =
   mk_fp_iter_fun_types
   #> map3 mk_fun_arg_typess ns mss
   #> map (map (map (unzip_recT fpTs)));
 
-fun mk_fold_rec_args_types Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy =
+fun mk_fold_rec_args_types fpTs Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy =
   let
     val Css = map2 replicate ns Cs;
     val y_Tsss = map3 mk_fun_arg_typess ns mss ctor_fold_fun_Ts;
     val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
 

       lthy
       |> mk_Freess "f" g_Tss
       ||>> mk_Freesss "x" y_Tsss;
     val yssss = map (map (map single)) ysss;
 
-    (* ### *)
-    fun dest_rec_prodT (T as Type (@{type_name prod}, Us as [_, U])) =
-        if member (op =) Cs U then Us else [T]
-      | dest_rec_prodT T = [T];
-
     val z_Tssss =
-      map3 (fn n => fn ms => map2 (map dest_rec_prodT oo dest_tupleT) ms o
+      map3 (fn n => fn ms => map2 (map (unzip_recT fpTs) oo dest_tupleT) ms o
         dest_sumTN_balanced n o domain_type) ns mss ctor_rec_fun_Ts;
 
     val z_Tsss = map3 mk_fun_arg_typess ns mss ctor_rec_fun_Ts;
     val z_Tsss' = map (map (flat_rec I)) z_Tssss;
     val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css;

     val (fp_rec_fun_Ts, fp_recs) = mk_co_iters thy fp fpTs Cs fp_recs0
       |> `(mk_fp_iter_fun_types o hd);
 
     val ((fold_rec_args_types, unfold_corec_args_types), lthy') =
       if fp = Least_FP then
-        mk_fold_rec_args_types Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
+        mk_fold_rec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
         |>> (rpair NONE o SOME)
       else
         mk_unfold_corec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
         |>> (pair NONE o SOME)
   in

 
     val ctor_fold_fun_Ts = mk_fp_iter_fun_types (hd ctor_folds);
     val ctor_rec_fun_Ts = mk_fp_iter_fun_types (hd ctor_recs);
 
     val (((gss, _, _), (hss, _, _)), names_lthy0) =
-      mk_fold_rec_args_types Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy;
+      mk_fold_rec_args_types fpTs Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy;
 
     val ((((ps, ps'), xsss), us'), names_lthy) =
       names_lthy0
       |> mk_Frees' "P" (map mk_pred1T fpTs)
       ||>> mk_Freesss "x" ctr_Tsss