1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
     1.3 @@ -175,17 +175,20 @@
     1.4          fp_iter_thms, fp_rec_thms), lthy)) =
     1.5        fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
     1.6  
     1.7 -    val add_nested_bnf_names =
     1.8 +    fun add_nesty_bnf_names Us =
     1.9        let
    1.10          fun add (Type (s, Ts)) ss =
    1.11              let val (needs, ss') = fold_map add Ts ss in
    1.12                if exists I needs then (true, insert (op =) s ss') else (false, ss')
    1.13              end
    1.14 -          | add T ss = (member (op =) Bs T, ss);
    1.15 +          | add T ss = (member (op =) Us T, ss);
    1.16        in snd oo add end;
    1.17  
    1.18 -    val nested_bnfs =
    1.19 -      map_filter (bnf_of lthy) (fold (fold (fold add_nested_bnf_names)) ctr_TsssBs []);
    1.20 +    fun nesty_bnfs Us =
    1.21 +      map_filter (bnf_of lthy) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_TsssBs []);
    1.22 +
    1.23 +    val nesting_bnfs = nesty_bnfs As;
    1.24 +    val nested_bnfs = nesty_bnfs Bs;
    1.25  
    1.26      val timer = time (Timer.startRealTimer ());
    1.27  
    1.28 @@ -498,7 +501,7 @@
    1.29  
    1.30      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    1.31      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
    1.32 -    val map_ids = map map_id_of_bnf nested_bnfs;
    1.33 +    val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
    1.34  
    1.35      fun mk_map Ts Us t =
    1.36        let val (Type (_, Ts0), Type (_, Us0)) = strip_map_type (fastype_of t) |>> List.last in
    1.37 @@ -626,9 +629,11 @@
    1.38              val goal_recss = map5 (map4 o mk_goal_iter_like hss) hrecs xctrss hss xsss hxsss;
    1.39  
    1.40              val iter_tacss =
    1.41 -              map2 (map o mk_iter_like_tac pre_map_defs map_ids iter_defs) fp_iter_thms ctr_defss;
    1.42 +              map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms
    1.43 +                ctr_defss;
    1.44              val rec_tacss =
    1.45 -              map2 (map o mk_iter_like_tac pre_map_defs map_ids rec_defs) fp_rec_thms ctr_defss;
    1.46 +              map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
    1.47 +                ctr_defss;
    1.48            in
    1.49              (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.50                 goal_iterss iter_tacss,
    1.51 @@ -704,10 +709,10 @@
    1.52                map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss cshsss';
    1.53  
    1.54              val coiter_tacss =
    1.55 -              map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs
    1.56 +              map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs
    1.57                  ctr_defss;
    1.58              val corec_tacss =
    1.59 -              map3 (map oo mk_coiter_like_tac corec_defs map_ids) fp_rec_thms pre_map_defs
    1.60 +              map3 (map oo mk_coiter_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
    1.61                  ctr_defss;
    1.62            in
    1.63              (map2 (map2 (fn goal => fn tac =>

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
     2.3 @@ -53,7 +53,7 @@
     2.4    Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
     2.5  
     2.6  fun mk_induct_tac ctxt =
     2.7 -  Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)(*###*);
     2.8 +  Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt) (* FIXME: TODO *);
     2.9  
    2.10  val iter_like_thms =
    2.11    @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps