replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures

--- a/src/HOL/Code_Evaluation.thy	Wed Sep 15 08:58:34 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Wed Sep 15 11:30:31 2010 +0200
@@ -278,6 +278,7 @@
   "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
   by (simp only: term_of_anything)
 
+
 subsection {* Obfuscate *}
 
 print_translation {*
@@ -292,52 +293,47 @@
 end
 *}
 
-hide_const dummy_term App valapp
-hide_const (open) Const termify valtermify term_of term_of_num
 
-subsection {* Tracing of generated and evaluated code *}
-
-definition tracing :: "String.literal => 'a => 'a"
-where
-  [code del]: "tracing s x = x"
+subsection {* Evaluation setup *}
 
 ML {*
-structure Code_Evaluation =
+signature CODE_EVALUATION =
+sig
+  val eval_term: theory -> term -> term
+  val put_term: (unit -> term) -> Proof.context -> Proof.context
+  val tracing: string -> 'a -> 'a
+end;
+
+structure Code_Evaluation : CODE_EVALUATION =
 struct
 
-fun tracing s x = (Output.tracing s; x)
+structure Evaluation = Proof_Data (
+  type T = unit -> term
+  fun init _ () = error "Evaluation"
+);
+val put_term = Evaluation.put;
+
+fun tracing s x = (Output.tracing s; x);
+
+fun eval_term thy t = Code_Eval.eval NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
+  I thy (HOLogic.mk_term_of (fastype_of t) t) [];
 
 end
 *}
 
+setup {*
+  Value.add_evaluator ("code", Code_Evaluation.eval_term o ProofContext.theory_of)
+*}
+
+definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
+  [code del]: "tracing s x = x"
+
 code_const "tracing :: String.literal => 'a => 'a"
   (Eval "Code'_Evaluation.tracing")
 
-hide_const (open) tracing
 code_reserved Eval Code_Evaluation
 
-subsection {* Evaluation setup *}
-
-ML {*
-signature EVAL =
-sig
-  val eval_ref: (unit -> term) option Unsynchronized.ref
-  val eval_term: theory -> term -> term
-end;
-
-structure Eval : EVAL =
-struct
-
-val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
-
-fun eval_term thy t =
-  Code_Eval.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
-
-end;
-*}
-
-setup {*
-  Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
-*}
+hide_const dummy_term App valapp
+hide_const (open) Const termify valtermify term_of term_of_num tracing
 
 end

--- a/src/HOL/Library/Eval_Witness.thy	Wed Sep 15 08:58:34 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Wed Sep 15 11:30:31 2010 +0200
@@ -44,15 +44,6 @@
 instance bool :: ml_equiv ..
 instance list :: (ml_equiv) ml_equiv ..
 
-ML {*
-structure Eval_Witness_Method =
-struct
-
-val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE;
-
-end;
-*}
-
 oracle eval_witness_oracle = {* fn (cgoal, ws) =>
 let
   val thy = Thm.theory_of_cterm cgoal;
@@ -68,7 +59,7 @@
     | dest_exs _ _ = sys_error "dest_exs";
   val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
 in
-  if Code_Eval.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
+  if Code_Eval.eval NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws
   then Thm.cterm_of thy goal
   else @{cprop True} (*dummy*)
 end