src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

           (((gss, g_Tss, map (map (map single)) ysss), (hss, h_Tss, zssss)),
            ([], [], [], (([], []), [], [], []), (([], []), [], [], [])))
         end
       else
         let
+          (*avoid "'a itself" arguments in coiterators and corecursors*)
+          val mss' =  map (fn [0] => [1] | ms => ms) mss;
+
           val p_Tss =
             map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns;
 
           fun popescu_zip [] [fs] = fs
             | popescu_zip (p :: ps) (fs :: fss) = p :: fs @ popescu_zip ps fss;

           fun mk_types fun_Ts =
             let
               val f_sum_prod_Ts = map range_type fun_Ts;
               val f_prod_Tss = map2 dest_sumTN ns f_sum_prod_Ts;
               val f_Tsss =
-                map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss f_prod_Tss;
+                map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss' f_prod_Tss;
               val pf_Tss = map2 popescu_zip p_Tss f_Tsss
             in (f_sum_prod_Ts, f_prod_Tss, f_Tsss, pf_Tss) end;
 
           val (g_sum_prod_Ts, g_prod_Tss, g_Tsss, pg_Tss) = mk_types fp_iter_fun_Ts;
           val (h_sum_prod_Ts, h_prod_Tss, h_Tsss, ph_Tss) = mk_types fp_rec_fun_Ts;