1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 15:03:15 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 15:11:24 2013 +0200
     1.3 @@ -471,13 +471,13 @@
     1.4  
     1.5  fun define_fold_rec fold_only rec_only mk_binding fpTs As Cs ctor_fold ctor_rec no_defs_lthy =
     1.6    let
     1.7 -    val kk = find_index (curry (op =) (body_type (fastype_of ctor_fold))) Cs;
     1.8 -    val fpT = nth fpTs kk; (* ### can use dummyT? or steal it from ctor_fold etc? *)
     1.9 -    val C = nth Cs kk;
    1.10 +    val nn = length fpTs;
    1.11 +
    1.12 +    val fpT_to_C = snd (strip_typeN nn (fastype_of ctor_fold));
    1.13  
    1.14      fun generate_iter (suf, ctor_iter, (fss, f_Tss, xsss)) =
    1.15        let
    1.16 -        val res_T = fold_rev (curry (op --->)) f_Tss (fpT --> C);
    1.17 +        val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
    1.18          val binding = mk_binding suf;
    1.19          val spec =
    1.20            mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
    1.21 @@ -505,14 +505,14 @@
    1.22  fun define_unfold_corec cs ns cpss unfold_only corec_only mk_binding fpTs As Cs dtor_unfold
    1.23      dtor_corec no_defs_lthy =
    1.24    let
    1.25 -    val kk = find_index (curry (op =) (body_type (fastype_of dtor_unfold))) fpTs;
    1.26 -    val fpT = nth fpTs kk; (* ### can use dummyT? or steal it from ctor_fold etc? *)
    1.27 -    val C = nth Cs kk;
    1.28 +    val nn = length fpTs;
    1.29 +
    1.30 +    val C_to_fpT = snd (strip_typeN nn (fastype_of dtor_unfold));
    1.31  
    1.32      fun generate_coiter (suf, dtor_coiter, ((pfss, cqssss, cfssss),
    1.33          (f_sum_prod_Ts, f_Tsss, pf_Tss))) =
    1.34        let
    1.35 -        val res_T = fold_rev (curry (op --->)) pf_Tss (C --> fpT);
    1.36 +        val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
    1.37          val binding = mk_binding suf;
    1.38          val spec =
    1.39            mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),