1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 22:23:10 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 22:23:10 2012 +0200
     1.3 @@ -565,12 +565,12 @@
     1.4                  | i => [([], (i + 1, x))])
     1.5                | mk_raw_prem_prems _ _ = [];
     1.6  
     1.7 -            fun close_prem_prem (Free x') t =
     1.8 -              fold_rev Logic.all
     1.9 -                (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
    1.10 +            fun close_prem_prem xs t =
    1.11 +              fold_rev Logic.all (map Free (drop (nn + length xs)
    1.12 +                (rev (Term.add_frees t (map dest_Free xs @ phis'))))) t;
    1.13  
    1.14 -            fun mk_prem_prem (xysets, (j, x)) =
    1.15 -              close_prem_prem x (Logic.list_implies (map (fn (x', (y, set)) =>
    1.16 +            fun mk_prem_prem xs (xysets, (j, x)) =
    1.17 +              close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
    1.18                    HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
    1.19                  HOLogic.mk_Trueprop (nth phis (j - 1) $ x)));
    1.20  
    1.21 @@ -578,14 +578,12 @@
    1.22                let
    1.23                  val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
    1.24                  val pprems = maps (mk_raw_prem_prems names_lthy') xs;
    1.25 -              in
    1.26 -                (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))
    1.27 -              end;
    1.28 +              in (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end;
    1.29  
    1.30              val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
    1.31  
    1.32              fun mk_prem (xs, raw_pprems, concl) =
    1.33 -              fold_rev Logic.all xs (Logic.list_implies (map mk_prem_prem raw_pprems, concl));
    1.34 +              fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
    1.35  
    1.36              val goal =
    1.37                Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
    1.38 @@ -598,19 +596,19 @@
    1.39                  val buckets = Library.partition_list has_index 1 nn pprems;
    1.40                  val pps = map length buckets;
    1.41                in
    1.42 -                map (fn pprem as (_ (*xysets*), (kk, _)) =>
    1.43 +                map (fn pprem as (xysets, (kk, _)) =>
    1.44                    ((nth pps (kk - 1), find_index (curry (op =) pprem) (nth buckets (kk - 1)) + 1),
    1.45 -                   kk)) pprems
    1.46 +                   (length xysets, kk))) pprems
    1.47                end;
    1.48  
    1.49 -            val ppjjkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
    1.50 +            val ixsss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
    1.51  
    1.52              val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    1.53  
    1.54              val induct_thm =
    1.55                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
    1.56 -                mk_induct_tac ctxt ns mss ppjjkksss (flat ctr_defss) fld_induct'
    1.57 -                  nested_set_natural's pre_set_defss)
    1.58 +                mk_induct_tac ctxt ns mss ixsss (flat ctr_defss) fld_induct' nested_set_natural's
    1.59 +                  pre_set_defss)
    1.60                |> singleton (Proof_Context.export names_lthy lthy)
    1.61            in
    1.62              `(conj_dests nn) induct_thm