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 @@ -51,14 +51,15 @@
1.4 Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
1.5
1.6 val iter_like_thms =
1.7 - @{thms sum_map.simps sum.simps(5,6) convol_def case_unit map_pair_def split_conv id_def};
1.8 + @{thms case_unit comp_def convol_def id_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
1.9
1.10 fun mk_iter_like_tac iter_like_defs fld_iter_likes ctr_def pre_map_def ctxt =
1.11 Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN
1.12 - Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
1.13 + Local_Defs.unfold_tac ctxt iter_like_thms THEN
1.14 + rtac refl 1;
1.15
1.16 val coiter_like_ss = ss_only @{thms if_True if_False};
1.17 -val coiter_like_thms = @{thms sum_map.simps map_pair_def id_def prod.cases};
1.18 +val coiter_like_thms = @{thms id_def map_pair_def sum_map.simps prod.cases};
1.19
1.20 fun mk_coiter_like_tac coiter_like_defs fld_unf_coiter_like pre_map_def ctr_def ctxt =
1.21 Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN