diff -r 490f34774a9a -r dd1dd470690b src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 05 15:43:21 2013 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 05 15:43:22 2013 +0100
@@ -303,7 +303,7 @@
       with `(\<Inter>i. A i) = {}` show False by auto
     qed
     ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
-      using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (A i)"] by simp
+      using LIMSEQ_INF[of "\<lambda>i. \<mu>G (A i)"] by simp
   qed fact+
   then guess \<mu> .. note \<mu> = this
   show ?thesis