src/Tools/code/code_ml.ML
changeset 30970 3fe2e418a071
parent 30962 f5fd07c558f9
child 31049 396d4d6a1594
--- a/src/Tools/code/code_ml.ML	Fri Apr 24 08:24:52 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Fri Apr 24 08:24:54 2009 +0200
@@ -6,10 +6,8 @@
 
 signature CODE_ML =
 sig
-  val eval_term: string option -> string * (unit -> term) option ref
-    -> theory -> term -> string list -> term
   val eval: string option -> string * (unit -> 'a) option ref
-    -> theory -> term -> string list -> 'a
+    -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
   val target_Eval: string
   val setup: theory -> theory
 end;
@@ -957,7 +955,7 @@
 
 (* evaluation *)
 
-fun gen_eval eval some_target reff thy t args =
+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 "
@@ -976,10 +974,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 I evaluator t end;
-
-fun eval_term thy = gen_eval Code_Thingol.eval_term thy;
-fun eval thy = gen_eval Code_Thingol.eval thy;
+  in Code_Thingol.eval thy I postproc evaluator t end;
 
 
 (* instrumentalization by antiquotation *)