--- a/src/HOL/Probability/Measurable.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Probability/Measurable.thy Tue Feb 23 16:25:08 2016 +0100
@@ -581,7 +581,7 @@
shows "Measurable.pred M (\<lambda>x. \<exists>!i\<in>I. P i x)"
unfolding bex1_def by measurable
-lemma measurable_split_if[measurable (raw)]:
+lemma measurable_if_split[measurable (raw)]:
"(c \<Longrightarrow> Measurable.pred M f) \<Longrightarrow> (\<not> c \<Longrightarrow> Measurable.pred M g) \<Longrightarrow>
Measurable.pred M (if c then f else g)"
by simp