diff -r 2eae295c8fc3 -r 0442b3f45556 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Jul 20 23:59:09 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jul 24 16:50:46 2017 +0100
@@ -5305,8 +5305,7 @@
   }
   then show lintg: "l contour_integrable_on \<gamma>"
     apply (simp add: contour_integrable_on)
-    apply (blast intro: integrable_uniform_limit_real)
-    done
+    by (metis (mono_tags, lifting)integrable_uniform_limit_real) 
   { fix e::real
     define B' where "B' = B + 1"
     have B': "B' > 0" "B' > B" using  \<open>0 \<le> B\<close> by (auto simp: B'_def)