1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jun 17 16:15:15 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jun 17 19:32:05 2010 +0200
     1.3 @@ -5266,7 +5266,7 @@
     1.4      (* class constraint due to continuous_on_inverse *)
     1.5    shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
     1.6            \<Longrightarrow> s homeomorphic t"
     1.7 -  unfolding homeomorphic_def by(metis homeomorphism_compact)
     1.8 +  unfolding homeomorphic_def by (auto intro: homeomorphism_compact)
     1.9  
    1.10  text{* Preservation of topological properties.                                   *}
    1.11