--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jun 21 19:33:51 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Jun 22 18:15:44 2010 +0200
@@ -5284,7 +5284,7 @@
(* class constraint due to continuous_on_inverse *)
shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
\<Longrightarrow> s homeomorphic t"
- unfolding homeomorphic_def by(auto intro: homeomorphism_compact)
+ unfolding homeomorphic_def by (metis homeomorphism_compact)
text{* Preservation of topological properties. *}