# 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 *)