instance real_field < field_char_0;
instance star :: (field_char_0) field_char_0

--- a/src/HOL/NSA/HyperDef.thy	Fri Jul 11 09:03:25 2008 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Fri Jul 11 16:56:20 2008 +0200
@@ -85,6 +85,8 @@
 
 instance star :: (real_div_algebra) real_div_algebra ..
 
+instance star :: (field_char_0) field_char_0 ..
+
 instance star :: (real_field) real_field ..
 
 lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)"

--- 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 *}