diff -r 6608c4838ff9 -r fdbb2c55ffc2 src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Wed Sep 15 11:30:31 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Wed Sep 15 11:30:32 2010 +0200
@@ -7,7 +7,8 @@
 signature CODE_EVAL =
 sig
   val target: string
-  val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
+  val eval: string option
+    -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
     -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
   val setup: theory -> theory
 end;
@@ -39,7 +40,7 @@
 
 (** evaluation **)
 
-fun eval some_target reff postproc thy t args =
+fun eval some_target cookie postproc thy t args =
   let
     val ctxt = ProofContext.init_global thy;
     fun evaluator naming program ((_, (_, ty)), t) deps =
@@ -55,7 +56,7 @@
           (the_default target some_target) NONE "Code" [] naming program' [value_name];
         val value_code = space_implode " "
           (value_name' :: map (enclose "(" ")") args);
-      in ML_Context.evaluate ctxt false reff (program_code, value_code) end;
+      in ML_Context.value ctxt cookie (program_code, value_code) end;
   in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;