1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:52:17 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 22:54:37 2012 +0200
     1.3 @@ -8,13 +8,13 @@
     1.4  signature BNF_FP_SUGAR_TACTICS =
     1.5  sig
     1.6    val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
     1.7 -  val mk_coiter_like_tac: thm list -> thm -> thm -> thm -> Proof.context -> tactic
     1.8 +  val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
     1.9    val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
    1.10    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
    1.11      -> tactic
    1.12    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
    1.13    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
    1.14 -  val mk_iter_like_tac: thm list -> thm list -> thm -> thm -> Proof.context -> tactic
    1.15 +  val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
    1.16  end;
    1.17  
    1.18  structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
    1.19 @@ -51,20 +51,19 @@
    1.20    Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
    1.21  
    1.22  val iter_like_thms =
    1.23 -  @{thms case_unit comp_def convol_def id_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
    1.24 +  @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
    1.25 +      split_conv};
    1.26  
    1.27 -fun mk_iter_like_tac map_defs iter_like_defs fld_iter_like ctr_def ctxt =
    1.28 -  Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ map_defs) THEN
    1.29 -  Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
    1.30 +fun mk_iter_like_tac pre_map_defs map_id's iter_like_defs fld_iter_like ctr_def ctxt =
    1.31 +  Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_id's @
    1.32 +    iter_like_thms) THEN rtac refl 1;
    1.33  
    1.34  val coiter_like_ss = ss_only @{thms if_True if_False};
    1.35 -val coiter_like_thms = @{thms id_def map_pair_def sum_map.simps prod.cases};
    1.36 +val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
    1.37  
    1.38 -fun mk_coiter_like_tac coiter_like_defs fld_unf_coiter_like pre_map_def ctr_def ctxt =
    1.39 +fun mk_coiter_like_tac coiter_like_defs map_id's fld_unf_coiter_like pre_map_def ctr_def ctxt =
    1.40    Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
    1.41 -  subst_tac ctxt [fld_unf_coiter_like] 1 THEN
    1.42 -  asm_simp_tac coiter_like_ss 1 THEN
    1.43 -  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms) THEN
    1.44 -  rtac refl 1;
    1.45 +  subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
    1.46 +  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_id's) THEN rtac refl 1;
    1.47  
    1.48  end;