diff -r bf99ccf71b7c -r 4ea3358fac3f src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Wed Dec 31 00:01:51 2008 +0100
+++ b/src/Tools/code/code_ml.ML	Wed Dec 31 00:08:11 2008 +0100
@@ -954,7 +954,7 @@
 fun eval eval'' term_of reff thy ct args =
   let
     val ctxt = ProofContext.init thy;
-    val _ = if null (term_frees (term_of ct)) then () else error ("Term "
+    val _ = if null (Term.add_frees (term_of ct) []) then () else error ("Term "
       ^ quote (Syntax.string_of_term_global thy (term_of ct))
       ^ " to be evaluated contains free variables");
     fun eval' naming program ((vs, ty), t) deps =