diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -12,7 +12,7 @@
   by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
      (force intro: exI[of _ "restrict f I" for f])
 
-lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
+lemma case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
   by auto
 
 subsubsection {* More about Function restricted by @{const extensional}  *}
@@ -1110,7 +1110,7 @@
 qed (simp add: space_PiM)
 
 lemma (in product_sigma_finite) product_nn_integral_pair:
-  assumes [measurable]: "split f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
+  assumes [measurable]: "case_prod f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
   assumes xy: "x \<noteq> y"
   shows "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {x, y} M) = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
 proof-