diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Oct 13 09:21:15 2015 +0200
@@ -943,7 +943,7 @@
     val CR = mk_bnf_T Ds RTs Calpha;
     val setRs =
       @{map 3} (fn R => fn T => fn U =>
-          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As Bs;
+          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_case_prod R) Rs As Bs;
 
     (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
       Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
@@ -1301,7 +1301,7 @@
                 val ran_bnfT = mk_bnf_T ranTs Calpha;
                 val (revTs, Ts) = `rev (bd_bnfT :: funTs);
                 val cTs = map (SOME o Thm.ctyp_of lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
-                val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs)
+                val tinst = fold (fn T => fn t => HOLogic.mk_case_prod (Term.absdummy T t)) (tl revTs)
                   (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
                     map Bound (live - 1 downto 0)) $ Bound live));
                 val cts = [NONE, SOME (Thm.cterm_of lthy tinst)];