--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Thu Jan 17 14:15:10 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Thu Jan 17 11:57:17 2013 +0100
@@ -57,7 +57,7 @@
apply (rule convex_connected, rule convex_real_interval)
done
-lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g :: 'a::metric_space set)"
+lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g)"
unfolding path_def path_image_def
by (erule compact_continuous_image, rule compact_interval)