src/HOL/Codegenerator_Test/code_test.ML

   val end_markerN : string
   val test_terms : Proof.context -> term list -> string -> unit
   val test_targets : Proof.context -> term list -> string list -> unit list
   val test_code_cmd : string list -> string list -> Toplevel.state -> unit
 
-  val eval_term : Proof.context -> term -> string -> unit
+  val eval_term : string -> Proof.context -> term -> term
 
   val gen_driver :
    (theory -> Path.T -> string list -> string ->
     {files : (Path.T * string) list,
      compile_cmd : string option, run_cmd : string, mk_code_file : string -> Path.T})

       Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
   in
     test_targets ctxt ts targets; ()
   end
 
-
-fun eval_term ctxt t target =
-  let
+fun eval_term target ctxt t =
+  let
+    val frees = Term.add_free_names t []
+    val _ = if frees = [] then () else
+      error ("Term contains free variables: " ^
+      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
+
     val thy = Proof_Context.theory_of ctxt
 
     val T_t = fastype_of t
     val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error 
       ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^ 

 
     val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
     val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
 
     val result = dynamic_value_strict ctxt t' target;
-    val t_eval = case result of [(_, SOME [t])] => t | _ => error "Evaluation failed"
-  in
-    Pretty.writeln (Syntax.pretty_term ctxt t_eval)
-  end
-
-fun eval_term_cmd raw_t target state =
-  let
-    val ctxt = Toplevel.context_of state;
-    val t = Syntax.read_term ctxt raw_t;
-    val frees = Term.add_free_names t []
-    val _ = if frees = [] then () else
-      error ("Term contains free variables: " ^
-      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
-  in
-    eval_term ctxt t target
-  end
-
+  in
+    case result of [(_, SOME [t])] => t | _ => error "Evaluation failed"
+  end
 
 (* Generic driver *)
 
 fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
   let

 val _ = 
   Outer_Syntax.command @{command_spec "test_code"}
     "compile test cases to target languages, execute them and report results"
       (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
 
-val eval_termP = Parse.term -- (@{keyword "in"} |-- Parse.name)
-
-val _ = 
-  Outer_Syntax.command @{command_spec "eval_term"}
-    "evaluate term in target language"
-      (eval_termP >> (fn (raw_t, target) => Toplevel.keep (eval_term_cmd raw_t target)))
-
 val _ = Context.>> (Context.map_theory (
   fold add_driver
     [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
      (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
      (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
      (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
      (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
-     (scalaN, (evaluate_in_scala, Code_Scala.target))]))
+     (scalaN, (evaluate_in_scala, Code_Scala.target))]
+    #> fold (fn target => Value.add_evaluator (target, eval_term target))
+      [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]
+    ))
 end