diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Lebesgue_Measure.thy
--- 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