1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 15 20:14:29 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 15 21:10:26 2012 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5      Copyright   2012
     1.6  
     1.7 -Sugar for constructing LFPs and GFPs.
     1.8 +Sugared datatype and codatatype constructions.
     1.9  *)
    1.10  
    1.11  signature BNF_FP_SUGAR =
    1.12 @@ -580,11 +580,11 @@
    1.13                  val pprems = maps (mk_raw_prem_prems names_lthy') xs;
    1.14                in (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end;
    1.15  
    1.16 -            val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
    1.17 -
    1.18              fun mk_prem (xs, raw_pprems, concl) =
    1.19                fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
    1.20  
    1.21 +            val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
    1.22 +
    1.23              val goal =
    1.24                Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
    1.25                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    1.26 @@ -601,14 +601,14 @@
    1.27                     (length xysets, kk))) pprems
    1.28                end;
    1.29  
    1.30 -            val ixsss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
    1.31 +            val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
    1.32  
    1.33              val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    1.34  
    1.35              val induct_thm =
    1.36                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
    1.37 -                mk_induct_tac ctxt ns mss ixsss (flat ctr_defss) fld_induct' nested_set_natural's
    1.38 -                  pre_set_defss)
    1.39 +                mk_induct_tac ctxt ns mss ppjjqqkksss (flat ctr_defss) fld_induct'
    1.40 +                  nested_set_natural's pre_set_defss)
    1.41                |> singleton (Proof_Context.export names_lthy lthy)
    1.42            in
    1.43              `(conj_dests nn) induct_thm