src/Tools/code/code_ml.ML
changeset 31063 88aaab83b6fc
parent 31054 841c9f67f9e7
child 31121 f79a0d03b75f
--- a/src/Tools/code/code_ml.ML	Thu May 07 16:22:34 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Thu May 07 16:22:35 2009 +0200
@@ -958,10 +958,7 @@
 fun eval some_target reff postproc thy t args =
   let
     val ctxt = ProofContext.init thy;
-    val _ = if null (Term.add_frees t []) then () else error ("Term "
-      ^ quote (Syntax.string_of_term_global thy t)
-      ^ " to be evaluated contains free variables");
-    fun evaluator naming program (((_, (_, ty)), _), t) deps =
+    fun evaluator naming program ((_, (_, ty)), t) deps =
       let
         val _ = if Code_Thingol.contains_dictvar t then
           error "Term to be evaluated contains free dictionaries" else ();