src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

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