add target language evaluators for the value command;
drop obsolete command eval_term

--- a/src/HOL/Codegenerator_Test/Code_Test.thy	Mon Sep 15 18:12:09 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test.thy	Tue Sep 16 16:04:08 2014 +0200
@@ -6,7 +6,7 @@
 
 theory Code_Test
 imports Main
-keywords "test_code" "eval_term" :: diag
+keywords "test_code" :: diag
 begin
 
 subsection {* YXML encoding for @{typ Code_Evaluation.term} *}

--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Mon Sep 15 18:12:09 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Tue Sep 16 16:04:08 2014 +0200
@@ -10,6 +10,6 @@
 
 test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC
 
-eval_term "14 + 7 * -12 :: integer" in GHC
+value [GHC] "14 + 7 * -12 :: integer"
 
 end

--- a/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Mon Sep 15 18:12:09 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Tue Sep 16 16:04:08 2014 +0200
@@ -8,6 +8,6 @@
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton
 
-eval_term "14 + 7 * -12 :: integer" in MLton
+value [MLton] "14 + 7 * -12 :: integer"
 
 end

--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Mon Sep 15 18:12:09 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Tue Sep 16 16:04:08 2014 +0200
@@ -8,6 +8,6 @@
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
 
-eval_term "14 + 7 * -12 :: integer" in OCaml
+value [OCaml] "14 + 7 * -12 :: integer"
 
 end

--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Mon Sep 15 18:12:09 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Tue Sep 16 16:04:08 2014 +0200
@@ -8,6 +8,6 @@
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML
 
-eval_term "14 + 7 * -12 :: integer" in PolyML
+value [PolyML] "14 + 7 * -12 :: integer"
 
 end

--- a/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Mon Sep 15 18:12:09 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Tue Sep 16 16:04:08 2014 +0200
@@ -8,6 +8,6 @@
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ
 
-eval_term "14 + 7 * -12 :: integer" in SMLNJ
+value [SMLNJ] "14 + 7 * -12 :: integer"
 
 end

--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Mon Sep 15 18:12:09 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Tue Sep 16 16:04:08 2014 +0200
@@ -8,6 +8,6 @@
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
 
-eval_term "14 + 7 * -12 :: integer" in Scala
+value [Scala] "14 + 7 * -12 :: integer"
 
 end

--- a/src/HOL/Codegenerator_Test/code_test.ML	Mon Sep 15 18:12:09 2014 +0200
+++ b/src/HOL/Codegenerator_Test/code_test.ML	Tue Sep 16 16:04:08 2014 +0200
@@ -16,7 +16,7 @@
   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 ->
@@ -252,9 +252,13 @@
     test_targets ctxt ts targets; ()
   end
 
+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))))
 
-fun eval_term ctxt t target =
-  let
     val thy = Proof_Context.theory_of ctxt
 
     val T_t = fastype_of t
@@ -266,24 +270,10 @@
     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)
+    case result of [(_, SOME [t])] => t | _ => error "Evaluation failed"
   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
-
-
 (* Generic driver *)
 
 fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
@@ -575,13 +565,6 @@
     "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)),
@@ -589,6 +572,9 @@
      (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