--- 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 =
--- 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 =