--- 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 =