diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Sun Feb 19 11:58:51 2017 +0100
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Tue Feb 21 15:04:01 2017 +0000
@@ -190,9 +190,9 @@
   have "g \<in> bcontfun"  \<comment> \<open>The limit function is bounded and continuous\<close>
   proof (intro bcontfunI)
     show "continuous_on UNIV g"
-      using bcontfunE[OF Rep_bcontfun] limit_function
-      by (intro continuous_uniform_limit[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"])
-        (auto simp add: eventually_sequentially trivial_limit_def dist_norm)
+      apply (rule bcontfunE[OF Rep_bcontfun])
+      using limit_function
+      by (auto simp add: uniform_limit_sequentially_iff intro: uniform_limit_theorem[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"])
   next
     fix x
     from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1"