1.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -958,7 +958,7 @@
     1.4          val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs));
     1.5          val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
     1.6        in
     1.7 -        HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
     1.8 +        HOLogic.mk_case_prod (Term.absfree Kl' (Term.absfree lab'
     1.9            (mk_case_sumN fs $ (lab $ HOLogic.mk_list sum_sbdT []))))
    1.10        end;
    1.11  
    1.12 @@ -2280,7 +2280,7 @@
    1.13          ||>> mk_Frees' "z" zip_zTs;
    1.14  
    1.15        val Iphi_sets =
    1.16 -        map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_split phi) allJphis zip_ranTs;
    1.17 +        map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_case_prod phi) allJphis zip_ranTs;
    1.18        val in_phis = map2 (mk_in Iphi_sets) (mk_setss zip_ranTs) zipFTs;
    1.19        val fstABs = map fst_const passiveABs;
    1.20        val all_fsts = fstABs @ fstsTsTs';
    1.21 @@ -2295,7 +2295,7 @@
    1.22          Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveBs @ Ts') bnf, all_snds)) Dss bnfs;
    1.23        val Jmap_snds = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T
    1.24          else Term.list_comb (map, sndABs)) (mk_Jmaps passiveABs passiveBs) Ts;
    1.25 -      val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_split zips)) ks;
    1.26 +      val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_case_prod zips)) ks;
    1.27        val zip_setss = mk_Jsetss passiveABs |> transpose;
    1.28  
    1.29        fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} =