--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 16 15:06:34 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 16 15:03:23 2009 +0100
@@ -5629,7 +5629,7 @@
moreover
have "d \<subseteq> ?D" unfolding subset_eq using assms by auto
hence *:"inj_on (basis::'n\<Rightarrow>real^'n) d" using subset_inj_on[OF basis_inj, of "d"] by auto
- have "?B hassize (card d)" unfolding hassize_def and card_image[OF *] by auto
+ have "card ?B = card d" unfolding card_image[OF *] by auto
ultimately show ?thesis using dim_unique[of "basis ` d" ?A] by auto
qed