# HG changeset patch
# User haftmann
# Date 1276795925 -7200
# Node ID 8f515d6aded5cde0c577905e26b8b884e4184183
# Parent  3058c918e7a3b25b3cf20b98313d15ec476a0a49
replaced unreliable metis proof

diff -r 3058c918e7a3 -r 8f515d6aded5 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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.                                   *}