--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jun 17 16:15:15 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jun 17 19:32:05 2010 +0200
@@ -5266,7 +5266,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(metis homeomorphism_compact)
+ unfolding homeomorphic_def by (auto intro: homeomorphism_compact)
text{* Preservation of topological properties. *}