1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 19:05:53 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 19:57:20 2012 +0200
     1.3 @@ -535,10 +535,10 @@
     1.4            let
     1.5              fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
     1.6  
     1.7 -            fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr cfs' =
     1.8 +            fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfs' =
     1.9                fold_rev (fold_rev Logic.all) ([c] :: pfss)
    1.10                  (Logic.list_implies (seq_conds mk_goal_cond n k cps,
    1.11 -                   mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, cfs'))));
    1.12 +                   mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs'))));
    1.13  
    1.14              fun build_call fiter_likes maybe_tack (T, U) =
    1.15                if T = U then
    1.16 @@ -558,13 +558,13 @@
    1.17                else
    1.18                  cf;
    1.19  
    1.20 -            val cgsss = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss;
    1.21 -            val chsss = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) chsss;
    1.22 +            val cgsss' = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss;
    1.23 +            val chsss' = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) chsss;
    1.24  
    1.25              val goal_coiterss =
    1.26 -              map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss;
    1.27 +              map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss cgsss';
    1.28              val goal_corecss =
    1.29 -              map7 (map3 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss chsss;
    1.30 +              map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss chsss';
    1.31  
    1.32              val coiter_tacss =
    1.33                map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 19:05:53 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 19:57:20 2012 +0200
     2.3 @@ -65,6 +65,7 @@
     2.4    Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
     2.5    subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
     2.6    Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
     2.7 -  Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
     2.8 +  Local_Defs.unfold_tac ctxt @{thms id_def} THEN
     2.9 +  (rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1;
    2.10  
    2.11  end;