--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sun Sep 09 19:05:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sun Sep 09 19:57:20 2012 +0200
@@ -535,10 +535,10 @@
let
fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
- fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr cfs' =
+ fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfs' =
fold_rev (fold_rev Logic.all) ([c] :: pfss)
(Logic.list_implies (seq_conds mk_goal_cond n k cps,
- mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, cfs'))));
+ mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs'))));
fun build_call fiter_likes maybe_tack (T, U) =
if T = U then
@@ -558,13 +558,13 @@
else
cf;
- val cgsss = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss;
- val chsss = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) chsss;
+ val cgsss' = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss;
+ val chsss' = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) chsss;
val goal_coiterss =
- map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss;
+ map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss cgsss';
val goal_corecss =
- map7 (map3 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss chsss;
+ map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss chsss';
val coiter_tacss =
map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Sun Sep 09 19:05:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Sun Sep 09 19:57:20 2012 +0200
@@ -65,6 +65,7 @@
Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
- Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
+ Local_Defs.unfold_tac ctxt @{thms id_def} THEN
+ (rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1;
end;