diff -r 253c98aa935a -r 409ca22dee4c src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Limits.thy	Wed Oct 06 14:19:46 2021 +0200
@@ -1000,7 +1000,7 @@
   unfolding tendsto_iff by simp
 
 lemma tendsto_add_const_iff:
-  "((\<lambda>x. c + f x :: 'a::real_normed_vector) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
+  "((\<lambda>x. c + f x :: 'a::topological_group_add) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
   using tendsto_add[OF tendsto_const[of c], of f d]
     and tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto