diff -r 7c8eb32724ce -r 88f0125c3bd2 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon May 03 17:13:37 2010 -0700
+++ b/src/HOL/Limits.thy	Mon May 03 17:39:46 2010 -0700
@@ -585,7 +585,7 @@
 unfolding tendsto_def eventually_at_topological by auto
 
 lemma tendsto_ident_at_within [tendsto_intros]:
-  "a \<in> S \<Longrightarrow> ((\<lambda>x. x) ---> a) (at a within S)"
+  "((\<lambda>x. x) ---> a) (at a within S)"
 unfolding tendsto_def eventually_within eventually_at_topological by auto
 
 lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) net"