diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Dec 29 23:04:53 2015 +0100
@@ -187,7 +187,7 @@
 
 lemma measure_PiM_countable:
   fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets M"
-  shows "(\<lambda>n. \<Prod>i\<le>n. measure M (E i)) ----> measure S (Pi UNIV E)"
+  shows "(\<lambda>n. \<Prod>i\<le>n. measure M (E i)) \<longlonglongrightarrow> measure S (Pi UNIV E)"
 proof -
   let ?E = "\<lambda>n. emb UNIV {..n} (Pi\<^sub>E {.. n} E)"
   have "\<And>n. (\<Prod>i\<le>n. measure M (E i)) = measure S (?E n)"