--- a/src/HOL/Probability/ex/Measure_Not_CCC.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy Tue Feb 23 16:25:08 2016 +0100
@@ -110,7 +110,7 @@
show "(\<Union>i. X i) \<in> sets M" "countable (\<Union>i. J i)" "G \<in> (\<Union>i. J i) \<rightarrow> sets M"
using XFJ by (auto simp: G_def Pi_iff)
show "UNION UNIV A = (UNIV - (\<Union>i. J i)) \<times> (\<Union>i. X i) \<union> (SIGMA j:\<Union>i. J i. \<Union>i. if j \<in> J i then F i j else X i)"
- unfolding A_eq by (auto split: split_if_asm)
+ unfolding A_eq by (auto split: if_split_asm)
qed
qed