diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -2335,7 +2335,7 @@
       then have eq: "(\<Union>i. F i) = F i"
         by auto
       with i show ?thesis
-        by (auto intro!: Lim_transform_eventually[OF _ tendsto_const] eventually_sequentiallyI[where c=i])
+        by (auto intro!: Lim_transform_eventually[OF tendsto_const] eventually_sequentiallyI[where c=i])
     next
       assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
       then obtain f where f: "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis