diff -r 042c2b3ea2d0 -r 34dc65df7014 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Tue May 11 17:20:11 2010 -0700
+++ b/src/HOL/RealVector.thy	Tue May 11 18:06:58 2010 -0700
@@ -5,7 +5,7 @@
 header {* Vector Spaces and Algebras over the Reals *}
 
 theory RealVector
-imports RealPow
+imports RComplete
 begin
 
 subsection {* Locale for additive functions *}