diff -r 0f38c96a0a74 -r bb29e4eb938d src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Aug 27 12:14:46 2020 +0100
+++ b/src/HOL/Limits.thy	Thu Aug 27 15:23:48 2020 +0100
@@ -2178,7 +2178,7 @@
 
 text \<open>A congruence rule allowing us to transform limits assuming not at point.\<close>
 
-lemma Lim_cong_within [cong]:
+lemma Lim_cong_within:
   assumes "a = b"
     and "x = y"
     and "S = T"