diff -r cf14976d4fdb -r 83b114a6545f src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Fri Dec 25 11:44:18 2020 +0000
+++ b/src/HOL/Analysis/Gamma_Function.thy	Fri Dec 25 15:37:27 2020 +0000
@@ -643,7 +643,8 @@
   assumes "summable (\<lambda>n. f (n + k) :: 'a :: real_normed_vector)"
   shows   "summable f"
 proof -
-  from assms have "convergent (\<lambda>m. \<Sum>n<m. f (n + k))" by (simp add: summable_iff_convergent)
+  from assms have "convergent (\<lambda>m. \<Sum>n<m. f (n + k))"
+    using summable_iff_convergent by blast
   hence "convergent (\<lambda>m. (\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)))"
     by (intro convergent_add convergent_const)
   also have "(\<lambda>m. (\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k))) = (\<lambda>m. \<Sum>n<m+k. f n)"