diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -559,12 +559,12 @@
   by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space)
 
 lemma measurable_distr2:
-  assumes f[measurable]: "split f \<in> measurable (L \<Otimes>\<^sub>M M) N"
+  assumes f[measurable]: "case_prod f \<in> measurable (L \<Otimes>\<^sub>M M) N"
   assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"
   shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"
 proof -
   have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
-    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)"
+    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (case_prod f)) \<in> measurable L (subprob_algebra N)"
   proof (rule measurable_cong)
     fix x assume x: "x \<in> space L"
     have gx: "g x \<in> space (subprob_algebra M)"
@@ -580,7 +580,7 @@
       using gx by (simp add: space_subprob_algebra)
     have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
       by (simp add: space_pair_measure)
-    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r")
+    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (case_prod f)" (is "?l = ?r")
     proof (rule measure_eqI)
       show "sets ?l = sets ?r"
         by simp
@@ -1150,7 +1150,7 @@
 
 lemma measurable_bind':
   assumes M1: "f \<in> measurable M (subprob_algebra N)" and
-          M2: "split g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
+          M2: "case_prod g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
   shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
 proof (subst measurable_cong)
   fix x assume x_in_M: "x \<in> space M"
@@ -1445,7 +1445,7 @@
 lemma double_bind_assoc:
   assumes Mg: "g \<in> measurable N (subprob_algebra N')"
   assumes Mf: "f \<in> measurable M (subprob_algebra M')"
-  assumes Mh: "split h \<in> measurable (M \<Otimes>\<^sub>M M') N"
+  assumes Mh: "case_prod h \<in> measurable (M \<Otimes>\<^sub>M M') N"
   shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g"
 proof-
   have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g =