# HG changeset patch
# User haftmann
# Date 1239950093 -7200
# Node ID 705bb15b236508eef0b33b1b581a6007baba8eca
# Parent  663af91c072045bf978811fbe8a1f1e2adb3a3b1
simplified code

diff -r 663af91c0720 -r 705bb15b2365 src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Fri Apr 17 08:34:52 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Fri Apr 17 08:34:53 2009 +0200
@@ -951,13 +951,13 @@
 
 (* evaluation *)
 
-fun eval eval'' term_of reff thy ct args =
+fun eval_term reff thy t args =
   let
     val ctxt = ProofContext.init thy;
-    val _ = if null (Term.add_frees (term_of ct) []) then () else error ("Term "
-      ^ quote (Syntax.string_of_term_global thy (term_of ct))
+    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 eval' naming program ((vs, 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 ();
@@ -970,9 +970,7 @@
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
       in ML_Context.evaluate ctxt false reff sml_code end;
-  in eval'' thy (rpair eval') ct end;
-
-fun eval_term reff = eval Code_Thingol.eval_term I reff;
+  in Code_Thingol.eval_term thy I evaluator t end;
 
 
 (* instrumentalization by antiquotation *)