src/HOL/Probability/Infinite_Product_Measure.thy

         then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) }
       then have "w' \<in> (\<Inter>i. A i)" by auto
       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
   proof (subst emeasure_extend_measure_Pair[OF PiM_def, of I M \<mu> J X])
     from assms show "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))"