diff -r 15cf4ed9c2a1 -r d315a513a150 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Fri Jul 11 09:03:25 2008 +0200
+++ b/src/HOL/Real/RealVector.thy	Fri Jul 11 16:56:20 2008 +0200
@@ -261,6 +261,8 @@
     by (simp only: of_real_of_nat_eq)
 qed
 
+instance real_field < field_char_0 ..
+
 
 subsection {* The Set of Real Numbers *}