--- a/src/HOL/Probability/Discrete_Topology.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy Tue Feb 23 16:25:08 2016 +0100
@@ -34,7 +34,7 @@
proof
fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X"
hence "\<exists>n. \<forall>m\<ge>n. X n = X m"
- by (force simp: dist_discrete_def Cauchy_def split: split_if_asm dest:spec[where x=1])
+ by (force simp: dist_discrete_def Cauchy_def split: if_split_asm dest:spec[where x=1])
then guess n ..
thus "convergent X"
by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n])