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 @@ -496,7 +496,6 @@
     1.4          ((wrap, define_iter_likes), lthy')
     1.5        end;
     1.6  
     1.7 -    (* TODO: remove all "nested" and "nesting" BNFs from pre_bnfs, if they're there ### *)
     1.8      val pre_map_defs = map map_def_of_bnf pre_bnfs;
     1.9      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
    1.10      val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
    1.11 @@ -572,7 +571,7 @@
    1.12                fold_rev Logic.all
    1.13                  (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
    1.14  
    1.15 -            fun mk_prem_triple phi ctr ctr_Ts =
    1.16 +            fun mk_raw_prem phi ctr ctr_Ts =
    1.17                let
    1.18                  val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
    1.19                  val prem_prems =
    1.20 @@ -581,17 +580,17 @@
    1.21                  (xs, prem_prems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))
    1.22                end;
    1.23  
    1.24 -            val prem_tripless = map3 (map2 o mk_prem_triple) phis ctrss ctr_Tsss;
    1.25 +            val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
    1.26  
    1.27              fun mk_prem (xs, prem_prems, concl) =
    1.28                fold_rev Logic.all xs (Logic.list_implies (prem_prems, concl));
    1.29  
    1.30              val goal =
    1.31 -              Library.foldr (Logic.list_implies o apfst (map mk_prem)) (prem_tripless,
    1.32 +              Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
    1.33                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    1.34                    (map2 (curry (op $)) phis vs)));
    1.35  
    1.36 -            val rss = map (map (length o #2)) prem_tripless;
    1.37 +            val rss = map (map (length o #2)) raw_premss;
    1.38  
    1.39              val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    1.40  
    1.41 @@ -672,7 +671,7 @@
    1.42      fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss,
    1.43          discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
    1.44        let
    1.45 -        val (vs', names_lthy) =
    1.46 +        val (vs', _) =
    1.47            lthy
    1.48            |> Variable.variant_fixes (map Binding.name_of fp_bs);
    1.49