1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Sun Sep 09 10:58:11 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Sun Sep 09 12:07:15 2012 +0200
1.3 @@ -54,16 +54,16 @@
1.4 @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
1.5 split_conv};
1.6
1.7 -fun mk_iter_like_tac pre_map_defs map_id's iter_like_defs fld_iter_like ctr_def ctxt =
1.8 - Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_id's @
1.9 +fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt =
1.10 + Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
1.11 iter_like_thms) THEN rtac refl 1;
1.12
1.13 val coiter_like_ss = ss_only @{thms if_True if_False};
1.14 val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
1.15
1.16 -fun mk_coiter_like_tac coiter_like_defs map_id's fld_unf_coiter_like pre_map_def ctr_def ctxt =
1.17 +fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt =
1.18 Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
1.19 subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
1.20 - Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_id's) THEN rtac refl 1;
1.21 + Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN rtac refl 1;
1.22
1.23 end;