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 @@ -13,7 +13,7 @@
     1.4      -> tactic
     1.5    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
     1.6    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
     1.7 -  val mk_iter_or_rec_tac: thm list -> thm list -> thm -> thm -> Proof.context -> tactic
     1.8 +  val mk_iter_like_tac: thm list -> thm list -> thm -> thm -> Proof.context -> tactic
     1.9  end;
    1.10  
    1.11  structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
    1.12 @@ -49,11 +49,11 @@
    1.13    Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
    1.14    Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
    1.15  
    1.16 -val iter_or_rec_thms =
    1.17 +val iter_like_thms =
    1.18    @{thms sum_map.simps sum.simps(5,6) convol_def case_unit map_pair_def split_conv id_def};
    1.19  
    1.20 -fun mk_iter_or_rec_tac iter_or_rec_defs fld_iter_or_recs ctr_def pre_map_def ctxt =
    1.21 -  Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_or_rec_defs @ fld_iter_or_recs) THEN
    1.22 -  Local_Defs.unfold_tac ctxt iter_or_rec_thms THEN rtac refl 1;
    1.23 +fun mk_iter_like_tac iter_like_defs fld_iter_likes ctr_def pre_map_def ctxt =
    1.24 +  Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN
    1.25 +  Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
    1.26  
    1.27  end;