diff -r 7c2c38a5bca3 -r 1e6206763036 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Mon Dec 07 14:54:28 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy	Mon Dec 07 16:27:48 2009 +0100
@@ -279,7 +279,7 @@
 val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
 
 fun eval_term thy t =
-  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
+  Code_Eval.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
 
 end;
 *}