diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -1075,24 +1075,6 @@
   unfolding nth_conv_component
   using component_le_infnorm[of x] .
 
-instance vec :: (perfect_space, finite) perfect_space
-proof
-  fix x :: "'a ^ 'b"
-  show "x islimpt UNIV"
-    apply (rule islimptI)
-    apply (unfold open_vec_def)
-    apply (drule (1) bspec)
-    apply clarsimp
-    apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>y. y \<in> A i \<and> y \<noteq> x $ i")
-     apply (drule finite_choice [OF finite_UNIV], erule exE)
-     apply (rule_tac x="vec_lambda f" in exI)
-     apply (simp add: vec_eq_iff)
-    apply (rule ballI, drule_tac x=i in spec, clarify)
-    apply (cut_tac x="x $ i" in islimpt_UNIV)
-    apply (simp add: islimpt_def)
-    done
-qed
-
 lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
 unfolding continuous_at by (intro tendsto_intros)