src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Feb 29 15:14:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Feb 29 16:35:15 2016 +0100
@@ -3437,7 +3437,7 @@
 qed
 
 lemma bounded_uminus [simp]:
-  fixes X :: "'a::euclidean_space set"
+  fixes X :: "'a::real_normed_vector set"
   shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
 by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)