1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 09 13:09:35 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 00:29:31 2011 -0700
     1.3 @@ -473,7 +473,7 @@
     1.4  using islimpt_UNIV [of x]
     1.5  by (simp add: islimpt_approachable)
     1.6  
     1.7 -instance real_basis_with_inner \<subseteq> perfect_space
     1.8 +instance euclidean_space \<subseteq> perfect_space
     1.9  proof
    1.10    fix x :: 'a
    1.11    { fix e :: real assume "0 < e"