# HG changeset patch
# User blanchet
# Date 1347185235 -7200
# Node ID d5717b5e2217f53f69e8e3eb8754275df40533bb
# Parent  e43910ccee74e45d388c8e386932fb29e6241cb4
use map_id, not map_id', to allow better composition

diff -r e43910ccee74 -r d5717b5e2217 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 10:58:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 12:07:15 2012 +0200
@@ -440,7 +440,7 @@
       end;
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
-    val map_id's = map map_id'_of_bnf nested_bnfs;
+    val map_ids = map map_id_of_bnf nested_bnfs;
 
     fun mk_map Ts Us t =
       let val (Type (_, Ts0), Type (_, Us0)) = strip_map_type (fastype_of t) |>> List.last in
@@ -500,9 +500,9 @@
             val goal_recss = map5 (map4 o mk_goal_iter_like hss) hrecs xctrss hss xsss hxsss;
 
             val iter_tacss =
-              map2 (map o mk_iter_like_tac pre_map_defs map_id's iter_defs) fp_iter_thms ctr_defss;
+              map2 (map o mk_iter_like_tac pre_map_defs map_ids iter_defs) fp_iter_thms ctr_defss;
             val rec_tacss =
-              map2 (map o mk_iter_like_tac pre_map_defs map_id's rec_defs) fp_rec_thms ctr_defss;
+              map2 (map o mk_iter_like_tac pre_map_defs map_ids rec_defs) fp_rec_thms ctr_defss;
           in
             (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
                goal_iterss iter_tacss,
@@ -549,7 +549,7 @@
               map7 (map3 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss chsss;
 
             val coiter_tacss =
-              map3 (map oo mk_coiter_like_tac coiter_defs map_id's) fp_iter_thms pre_map_defs
+              map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs
                 ctr_defss;
           in
             (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
diff -r e43910ccee74 -r d5717b5e2217 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 10:58:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 12:07:15 2012 +0200
@@ -54,16 +54,16 @@
   @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
       split_conv};
 
-fun mk_iter_like_tac pre_map_defs map_id's 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_id's @
+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;
 
 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};
 
-fun mk_coiter_like_tac coiter_like_defs map_id's fld_unf_coiter_like pre_map_def ctr_def ctxt =
+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_id's) THEN rtac refl 1;
+  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN rtac refl 1;
 
 end;