1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:21:27 2012 +0200
     1.3 @@ -222,6 +222,9 @@
     1.4          end
     1.5        else
     1.6          let
     1.7 +          (*avoid "'a itself" arguments in coiterators and corecursors*)
     1.8 +          val mss' =  map (fn [0] => [1] | ms => ms) mss;
     1.9 +
    1.10            val p_Tss =
    1.11              map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns;
    1.12  
    1.13 @@ -233,7 +236,7 @@
    1.14                val f_sum_prod_Ts = map range_type fun_Ts;
    1.15                val f_prod_Tss = map2 dest_sumTN ns f_sum_prod_Ts;
    1.16                val f_Tsss =
    1.17 -                map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss f_prod_Tss;
    1.18 +                map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss' f_prod_Tss;
    1.19                val pf_Tss = map2 popescu_zip p_Tss f_Tsss
    1.20              in (f_sum_prod_Ts, f_prod_Tss, f_Tsss, pf_Tss) end;
    1.21