1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 17 21:13:30 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 17 21:13:30 2012 +0200
     1.3 @@ -590,25 +590,13 @@
     1.4                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
     1.5                    (map2 (curry (op $)) phis vs)));
     1.6  
     1.7 -            fun mk_raw_prem_prems_indices pprems =
     1.8 -              let
     1.9 -                fun has_index kk (_, (kk', _)) = kk' = kk;
    1.10 -                val buckets = Library.partition_list has_index 1 nn pprems;
    1.11 -                val pps = map length buckets;
    1.12 -              in
    1.13 -                map (fn pprem as (xysets, (kk, _)) =>
    1.14 -                  ((nth pps (kk - 1), find_index (curry (op =) pprem) (nth buckets (kk - 1)) + 1),
    1.15 -                   (length xysets, kk))) pprems
    1.16 -              end;
    1.17 -
    1.18 -            val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
    1.19 -val _ = tracing ("val ppjjqqkksss = " ^ PolyML.makestring ppjjqqkksss) (*###*)
    1.20 +            val kksss = map (map (map (fst o snd) o #2)) raw_premss;
    1.21  
    1.22              val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    1.23  
    1.24              val induct_thm =
    1.25                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
    1.26 -                mk_induct_tac ctxt ns mss ppjjqqkksss (flat ctr_defss) fld_induct'
    1.27 +                mk_induct_tac ctxt ns mss kksss (flat ctr_defss) fld_induct'
    1.28                    nested_set_natural's pre_set_defss)
    1.29                |> singleton (Proof_Context.export names_lthy lthy)
    1.30            in