--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Sun Sep 09 13:04:57 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Sun Sep 09 17:14:39 2012 +0200
@@ -51,19 +51,19 @@
Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
val iter_like_thms =
- @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
- split_conv};
+ @{thms case_unit comp_def convol_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt =
Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
- iter_like_thms) THEN rtac refl 1;
+ iter_like_thms) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
val coiter_like_ss = ss_only @{thms if_True if_False};
-val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
+val coiter_like_thms = @{thms map_pair_def sum_map.simps prod.cases};
fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt =
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 rtac refl 1;
+ 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;
end;