src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

     (term list list
      * (typ list list * typ list list list list * term list list
         * term list list list list) list option
      * (term list * term list list
         * ((term list list * term list list list list * term list list list list)
-           * (typ list * typ list list list * typ list list))
-        * ((term list list * term list list list list * term list list list list)
-           * (typ list * typ list list list * typ list list))) option)
+           * (typ list * typ list list list * typ list list)) list) option)
     * Proof.context
   val mk_map: int -> typ list -> typ list -> term -> term
   val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
 
   val mk_iter_fun_arg_typessss: typ list -> int list -> int list list -> term ->
     typ list list list list
   val define_iters: string list ->
     (typ list list * typ list list list list * term list list * term list list list list) list ->
     (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
     (term list * thm list) * Proof.context
-  val define_coiters: term list * term list list
+  val define_coiters: string list -> term list * term list list
     * ((term list list * term list list list list * term list list list list)
-       * (typ list * typ list list list * typ list list))
-    * ((term list list * term list list list list * term list list list list)
-       * (typ list * typ list list list * typ list list)) ->
+       * (typ list * typ list list list * typ list list)) list ->
     (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
     (term list * thm list) * Proof.context
   val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list list ->
     (typ list list * typ list list list list * term list list * term list list list list) list ->
     thm -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->

       in (pfss, cqssss, cfssss) end;
 
     val unfold_args = mk_args rssss gssss;
     val corec_args = mk_args sssss hssss;
   in
-    ((cs, cpss, (unfold_args, unfold_types), (corec_args, corec_types)), lthy)
+    ((cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
   end;
 
 fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0' lthy =
   let
     val thy = Proof_Context.theory_of lthy;

     val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss;
   in
     Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss)
   end;
 
-fun define_iters iterNs iter_args_typess mk_binding fpTs Cs ctor_iters lthy0 =
+fun define_iters iterNs iter_args_typess' mk_binding fpTs Cs ctor_iters lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
     val nn = length fpTs;
 

         val spec =
           mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of b, res_T)),
             mk_iter_body ctor_iter fss xssss);
       in (b, spec) end;
 
-    val binding_specs = map3 generate_iter iterNs iter_args_typess ctor_iters;
+    val binding_specs = map3 generate_iter iterNs iter_args_typess' ctor_iters;
 
     val ((csts, defs), (lthy', lthy)) = lthy0
       |> apfst split_list o fold_map (fn (b, spec) =>
         Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
         #>> apsnd snd) binding_specs

   in
     ((iters, iter_defs), lthy')
   end;
 
 (* TODO: merge with above function? *)
-fun define_coiters (cs, cpss, unfold_args_types, corec_args_types) mk_binding fpTs Cs
-    [dtor_unfold, dtor_corec] lthy0 =
+fun define_coiters coiterNs (cs, cpss, coiter_args_typess') mk_binding fpTs Cs dtor_coiters lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
     val nn = length fpTs;
 
-    val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of dtor_unfold));
-
-    fun generate_coiter (suf, dtor_coiter, ((pfss, cqssss, cfssss),
-        (f_sum_prod_Ts, f_Tsss, pf_Tss))) =
+    val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
+
+    fun generate_coiter suf ((pfss, cqssss, cfssss), (f_sum_prod_Ts, f_Tsss, pf_Tss)) dtor_coiter =
       let
         val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
         val b = mk_binding suf;
         val spec =
           mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)),
             mk_coiter_body lthy0 cs cpss f_sum_prod_Ts f_Tsss cqssss cfssss dtor_coiter);
       in (b, spec) end;
 
-    val binding_specs =
-      map generate_coiter [(unfoldN, dtor_unfold, unfold_args_types),
-        (corecN, dtor_corec, corec_args_types)];
+    val binding_specs = map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters;
 
     val ((csts, defs), (lthy', lthy)) = lthy0
       |> apfst split_list o fold_map (fn (b, spec) =>
         Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
         #>> apsnd snd) binding_specs

     val exhausts = map #exhaust ctr_sugars;
     val disc_thmsss = map #disc_thmss ctr_sugars;
     val discIss = map #discIs ctr_sugars;
     val sel_thmsss = map #sel_thmss ctr_sugars;
 
-    val ((cs, cpss, ((pgss, crssss, cgssss), _), ((phss, csssss, chssss), _)), names_lthy0) =
+    val ((cs, cpss, [((pgss, crssss, cgssss), _), ((phss, csssss, chssss), _)]), names_lthy0) =
       mk_unfold_corec_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy;
 
     val (((rs, us'), vs'), names_lthy) =
       names_lthy0
       |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)

       in
         (wrap_ctrs
          #> derive_maps_sets_rels
          ##>>
            (if fp = Least_FP then define_iters [foldN, recN] (the fold_rec_args_types)
-            else define_coiters (the unfold_corec_args_types))
+            else define_coiters [unfoldN, corecN] (the unfold_corec_args_types))
              mk_binding fpTs Cs [xtor_un_fold, xtor_co_rec]
          #> massage_res, lthy')
       end;
 
     fun wrap_types_etc (wrap_types_etcs, lthy) =