diff -r 7feb35deb6f6 -r 5f13912245ff src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Wed Sep 23 13:42:53 2009 +0200
+++ b/src/HOL/RealDef.thy	Wed Sep 23 14:00:12 2009 +0200
@@ -1128,8 +1128,8 @@
   by (simp add: of_rat_divide)
 
 definition (in term_syntax)
-  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
-  [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+  [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
 
 notation fcomp (infixl "o>" 60)
 notation scomp (infixl "o\<rightarrow>" 60)