--- a/src/HOL/Probability/Lebesgue_Measure.thy Fri May 30 18:13:40 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri May 30 15:56:30 2014 +0200
@@ -740,7 +740,7 @@
show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) ----> f x"
using lim by auto
show "(\<lambda>k. integral\<^sup>L lebesgue (s k)) ----> integral\<^sup>L lebesgue f"
- using lim by (intro integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"]) auto
+ using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
qed
qed