# HG changeset patch
# User blanchet
# Date 1349081190 -7200
# Node ID 61729b1493972a692bf10a0fb3d5c1b2800cb29a
# Parent  c7a034d01936c24e7192dc922048dc710a5c2733
tweaked corecursor/coiterator tactic

diff -r c7a034d01936 -r 61729b149397 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 10:34:58 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 10:46:30 2012 +0200
@@ -281,8 +281,7 @@
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
     val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
     val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
-    val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def}) nesting_map_ids;
+    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
     val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
     val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs;
 
@@ -1002,10 +1001,10 @@
               map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
 
             val unfold_tacss =
-              map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids) fp_fold_thms pre_map_defs
-                ctr_defss;
+              map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids'') fp_fold_thms
+                pre_map_defs ctr_defss;
             val corec_tacss =
-              map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
+              map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids'') fp_rec_thms pre_map_defs
                 ctr_defss;
 
             fun prove goal tac =
diff -r c7a034d01936 -r 61729b149397 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Oct 01 10:34:58 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Oct 01 10:46:30 2012 +0200
@@ -107,11 +107,10 @@
   unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_comp's @
     map_ids'' @ rec_like_unfold_thms) THEN rtac refl 1;
 
-fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt =
+fun mk_corec_like_tac corec_like_defs map_ids'' ctor_dtor_corec_like pre_map_def ctr_def ctxt =
   unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN
   (rtac (ctor_dtor_corec_like RS trans) THEN' asm_simp_tac ss_if_True_False) 1 THEN
-  unfold_thms_tac ctxt (pre_map_def :: sum_prod_thms_map @ map_ids) THEN
-  unfold_thms_tac ctxt @{thms id_def} THEN
+  unfold_thms_tac ctxt (pre_map_def :: @{thm id_def} :: sum_prod_thms_map @ map_ids'') THEN
   (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)) 1;
 
 fun mk_disc_corec_like_iff_tac case_splits' corec_likes discs ctxt =