1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     1.3 @@ -53,10 +53,9 @@
     1.4  val iter_like_thms =
     1.5    @{thms case_unit comp_def convol_def id_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
     1.6  
     1.7 -fun mk_iter_like_tac iter_like_defs fld_iter_likes ctr_def pre_map_def ctxt =
     1.8 -  Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN
     1.9 -  Local_Defs.unfold_tac ctxt iter_like_thms THEN
    1.10 -  rtac refl 1;
    1.11 +fun mk_iter_like_tac map_defs iter_like_defs fld_iter_like ctr_def ctxt =
    1.12 +  Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ map_defs) THEN
    1.13 +  Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
    1.14  
    1.15  val coiter_like_ss = ss_only @{thms if_True if_False};
    1.16  val coiter_like_thms = @{thms id_def map_pair_def sum_map.simps prod.cases};