--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 24 15:03:50 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 24 15:03:51 2013 -0700
@@ -1528,7 +1528,7 @@
unfolding filter_eq_iff by (intro allI eventually_within_interior)
lemma Lim_within_LIMSEQ:
- fixes a :: "'a::metric_space"
+ fixes a :: "'a::first_countable_topology"
assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
shows "(X ---> L) (at a within T)"
using assms unfolding tendsto_def [where l=L]