src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 49671 61729b149397
parent 49670 c7a034d01936
child 49672 902b24e0ffb4
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 10:34:58 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 10:46:30 2012 +0200
     1.3 @@ -281,8 +281,7 @@
     1.4      val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
     1.5      val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
     1.6      val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
     1.7 -    val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
     1.8 -    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def}) nesting_map_ids;
     1.9 +    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
    1.10      val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
    1.11      val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs;
    1.12  
    1.13 @@ -1002,10 +1001,10 @@
    1.14                map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
    1.15  
    1.16              val unfold_tacss =
    1.17 -              map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids) fp_fold_thms pre_map_defs
    1.18 -                ctr_defss;
    1.19 +              map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids'') fp_fold_thms
    1.20 +                pre_map_defs ctr_defss;
    1.21              val corec_tacss =
    1.22 -              map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
    1.23 +              map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids'') fp_rec_thms pre_map_defs
    1.24                  ctr_defss;
    1.25  
    1.26              fun prove goal tac =