diff -r 0a2a1b6507c1 -r 493b818e8e10 src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Apr 18 21:12:50 2018 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed May 02 13:49:38 2018 +0200
@@ -1376,7 +1376,7 @@
       using \<open>polynomial_function g\<close>  by auto
     show "(\<lambda>x. \<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i) ` S \<subseteq> T"
       using \<open>B \<subseteq> T\<close>
-      by (blast intro: real_vector_class.subspace_sum subspace_mul \<open>subspace T\<close>)
+      by (blast intro: subspace_sum subspace_mul \<open>subspace T\<close>)
     show "norm (f x - (\<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i)) < e" if "x \<in> S" for x
     proof -
       have orth': "pairwise (\<lambda>i j. orthogonal ((f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i)