src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

         * term list list list list) list option
      * (string * term list * term list list
         * ((term list list * term list list list) * (typ list * typ list list)) list) option)
     * Proof.context
 
-  val mk_iter_fun_arg_types: typ list -> int list -> int list list -> term ->
+  val mk_iter_fun_arg_types: typ list list list -> int list -> int list list -> term ->
     typ list list list list
   val mk_coiter_fun_arg_types: typ list list list -> typ list -> int list -> term ->
     typ list list
     * (typ list list list list * typ list list list * typ list list list list * typ list)
   val define_iters: string list ->

     map (Term.subst_TVars rho) ts0
   end;
 
 val mk_fp_iter_fun_types = binder_fun_types o fastype_of;
 
-(* ### FIXME? *)
-fun unzip_recT Cs (T as Type (@{type_name prod}, Ts as [_, U])) =
-    if member (op =) Cs U then Ts else [T]
+fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
+  | unzip_recT _ (T as Type (@{type_name prod}, Ts)) = Ts
   | unzip_recT _ T = [T];
 
 fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
   | unzip_corecT _ (T as Type (@{type_name sum}, Ts)) = Ts
   | unzip_corecT _ T = [T];

 
 fun indexify proj xs f p = f (find_index (curry op = (proj p)) xs) p;
 
 fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
 
-fun mk_iter_fun_arg_types Cs ns mss =
+fun mk_iter_fun_arg_types ctr_Tsss ns mss =
   mk_fp_iter_fun_types
   #> map3 mk_iter_fun_arg_types0 ns mss
-  #> map (map (map (unzip_recT Cs)));
-
-fun mk_iters_args_types Cs ns mss ctor_iter_fun_Tss lthy =
+  #> map2 (map2 (map2 unzip_recT)) ctr_Tsss;
+
+fun mk_iters_args_types ctr_Tsss Cs ns mss ctor_iter_fun_Tss lthy =
   let
     val Css = map2 replicate ns Cs;
     val y_Tsss = map3 mk_iter_fun_arg_types0 ns mss (map un_fold_of ctor_iter_fun_Tss);
     val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
 

 
     val y_Tssss = map (map (map single)) y_Tsss;
     val yssss = map (map (map single)) ysss;
 
     val z_Tssss =
-      map3 (fn n => fn ms => map2 (map (unzip_recT Cs) oo dest_tupleT) ms o
-        dest_sumTN_balanced n o domain_type o co_rec_of) ns mss ctor_iter_fun_Tss;
+      map4 (fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts =>
+          map3 (fn m => fn ctr_Ts => fn ctor_iter_fun_T =>
+              map2 unzip_recT ctr_Ts (dest_tupleT m ctor_iter_fun_T))
+            ms ctr_Tss (dest_sumTN_balanced n (domain_type (co_rec_of ctor_iter_fun_Ts))))
+        ns mss ctr_Tsss ctor_iter_fun_Tss;
 
     val z_Tsss' = map (map flat_rec_arg_args) z_Tssss;
     val h_Tss = map2 (map2 (curry op --->)) z_Tsss' Css;
 
     val hss = map2 (map2 retype_free) h_Tss gss;

       map (mk_co_iters thy fp fpTs Cs #> `(mk_fp_iter_fun_types o hd)) (transpose xtor_co_iterss0)
       |> apsnd transpose o apfst transpose o split_list;
 
     val ((iters_args_types, coiters_args_types), lthy') =
       if fp = Least_FP then
-        mk_iters_args_types Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME)
+        mk_iters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME)
       else
         mk_coiters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME)
   in
     ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy')
   end;