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 xs t =
     1.8 +            fun close_prem_prem (Free x') t =
     1.9                fold_rev Logic.all
    1.10 -                (map Free (drop (2 * nn) (rev (Term.add_frees t (map dest_Free xs @ phis'))))) t;
    1.11 +                (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
    1.12  
    1.13 -            fun mk_prem_prem xs (xysets, (j, x)) =
    1.14 -              close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
    1.15 +            fun mk_prem_prem (xysets, (j, x)) =
    1.16 +              close_prem_prem x (Logic.list_implies (map (fn (x', (y, set)) =>
    1.17                    HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
    1.18                  HOLogic.mk_Trueprop (nth phis (j - 1) $ x)));
    1.19  
    1.20 @@ -585,23 +585,25 @@
    1.21              val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
    1.22  
    1.23              fun mk_prem (xs, raw_pprems, concl) =
    1.24 -              fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
    1.25 +              fold_rev Logic.all xs (Logic.list_implies (map mk_prem_prem raw_pprems, concl));
    1.26  
    1.27              val goal =
    1.28                Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
    1.29                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    1.30                    (map2 (curry (op $)) phis vs)));
    1.31  
    1.32 -            fun mk_prem_prems_indices raw_pprems =
    1.33 +            fun mk_raw_prem_prems_indices pprems =
    1.34                let
    1.35 -                val rr = length raw_pprems;
    1.36 +                fun has_index kk (_, (kk', _)) = kk' = kk;
    1.37 +                val buckets = Library.partition_list has_index 1 nn pprems;
    1.38 +                val pps = map length buckets;
    1.39                in
    1.40 -                map2 (fn pp => fn (xysets, (i, _)) => ((rr, pp), i)) (1 upto rr) raw_pprems
    1.41 +                map (fn pprem as (_ (*xysets*), (kk, _)) =>
    1.42 +                  ((nth pps (kk - 1), find_index (curry (op =) pprem) (nth buckets (kk - 1)) + 1),
    1.43 +                   kk)) pprems
    1.44                end;
    1.45  
    1.46 -            val ppjjkksss = map (map (mk_prem_prems_indices o #2)) raw_premss;
    1.47 -
    1.48 -val _ = tracing ("PPJJISSS:\n" ^ PolyML.makestring (ppjjkksss)) (*###*)
    1.49 +            val ppjjkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
    1.50  
    1.51              val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    1.52