src/Tools/Code/code_eval.ML

 *)
 
 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;
 
 structure Code_Eval : CODE_EVAL =

   in (ml_code, (tycos_map, consts_map)) end;
 
 
 (** 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 =
       let
         val _ = if Code_Thingol.contains_dictvar t then

           |> fold (curry Graph.add_edge value_name) deps;
         val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
           (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;
 
 
 (** instrumentalization by antiquotation **)