merged

--- a/src/HOL/Code_Evaluation.thy	Wed Sep 15 10:45:22 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Wed Sep 15 12:16:08 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/HOL.thy	Wed Sep 15 10:45:22 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Sep 15 12:16:08 2010 +0200
@@ -1966,12 +1966,10 @@
 *}
 
 ML {*
-structure Eval_Method =
-struct
-
-val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE;
-
-end;
+structure Eval_Method = Proof_Data(
+  type T = unit -> bool
+  fun init thy () = error "Eval_Method"
+)
 *}
 
 oracle eval_oracle = {* fn ct =>
@@ -1981,7 +1979,7 @@
     val dummy = @{cprop True};
   in case try HOLogic.dest_Trueprop t
    of SOME t' => if Code_Eval.eval NONE
-         ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] 
+         (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' [] 
        then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
        else dummy
     | NONE => dummy

--- a/src/HOL/Library/Eval_Witness.thy	Wed Sep 15 10:45:22 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Wed Sep 15 12:16:08 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

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 10:45:22 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 12:16:08 2010 +0200
@@ -43,18 +43,20 @@
   val print_stored_rules : Proof.context -> unit
   val print_all_modes : compilation -> Proof.context -> unit
   val mk_casesrule : Proof.context -> term -> thm list -> term
-  val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
-  val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
-    option Unsynchronized.ref
-  val dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref
-  val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int))
-    option Unsynchronized.ref
-  val new_random_dseq_eval_ref :
-    (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence)
-      option Unsynchronized.ref
-  val new_random_dseq_stats_eval_ref :
-    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence)
-      option Unsynchronized.ref
+
+  val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
+  val put_pred_random_result : (unit -> int * int -> term Predicate.pred * (int * int)) ->
+    Proof.context -> Proof.context
+  val put_dseq_result : (unit -> term DSequence.dseq) -> Proof.context -> Proof.context
+  val put_dseq_random_result : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) ->
+    Proof.context -> Proof.context
+  val put_lseq_random_result :
+    (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) ->
+    Proof.context -> Proof.context
+  val put_lseq_random_stats_result :
+    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) ->
+    Proof.context -> Proof.context
+
   val code_pred_intro_attrib : attribute
   (* used by Quickcheck_Generator *) 
   (* temporary for testing of the compilation *)
@@ -3105,17 +3107,41 @@
 
 (* transformation for code generation *)
 
-val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
-val random_eval_ref =
-  Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option);
-val dseq_eval_ref = Unsynchronized.ref (NONE : (unit -> term DSequence.dseq) option);
-val random_dseq_eval_ref =
-  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option);
-val new_random_dseq_eval_ref =
-  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) option)
-val new_random_dseq_stats_eval_ref =
-    Unsynchronized.ref (NONE :
-      (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) option)
+structure Pred_Result = Proof_Data (
+  type T = unit -> term Predicate.pred
+  fun init _ () = error "Pred_Result"
+);
+val put_pred_result = Pred_Result.put;
+
+structure Pred_Random_Result = Proof_Data (
+  type T = unit -> int * int -> term Predicate.pred * (int * int)
+  fun init _ () = error "Pred_Random_Result"
+);
+val put_pred_random_result = Pred_Random_Result.put;
+
+structure Dseq_Result = Proof_Data (
+  type T = unit -> term DSequence.dseq
+  fun init _ () = error "Dseq_Result"
+);
+val put_dseq_result = Dseq_Result.put;
+
+structure Dseq_Random_Result = Proof_Data (
+  type T = unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)
+  fun init _ () = error "Dseq_Random_Result"
+);
+val put_dseq_random_result = Dseq_Random_Result.put;
+
+structure Lseq_Random_Result = Proof_Data (
+  type T = unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence
+  fun init _ () = error "Lseq_Random_Result"
+);
+val put_lseq_random_result = Lseq_Random_Result.put;
+
+structure Lseq_Random_Stats_Result = Proof_Data (
+  type T = unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence
+  fun init _ () = error "Lseq_Random_Stats_Result"
+);
+val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put;
 
 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
 fun analyze_compr ctxt compfuns param_user_modes (compilation, arguments) t_compr =
@@ -3251,7 +3277,7 @@
             val [nrandom, size, depth] = arguments
           in
             rpair NONE (fst (DSequence.yieldn k
-              (Code_Eval.eval NONE ("Predicate_Compile_Core.random_dseq_eval_ref", random_dseq_eval_ref)
+              (Code_Eval.eval NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
                 (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
                   thy t' [] nrandom size
                 |> Random_Engine.run)
@@ -3259,7 +3285,7 @@
           end
       | DSeq =>
           rpair NONE (fst (DSequence.yieldn k
-            (Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref)
+            (Code_Eval.eval NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
               DSequence.map thy t' []) (the_single arguments) true))
       | New_Pos_Random_DSeq =>
           let
@@ -3270,21 +3296,21 @@
               apsnd (SOME o accumulate) (split_list
               (fst (Lazy_Sequence.yieldn k
                 (Code_Eval.eval NONE
-                  ("Predicate_Compile_Core.new_random_dseq_stats_eval_ref", new_random_dseq_stats_eval_ref)
+                  (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa (apfst proc))
                     thy t' [] nrandom size seed depth))))
             else rpair NONE
               (fst (Lazy_Sequence.yieldn k
                 (Code_Eval.eval NONE
-                  ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
+                  (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa proc)
                     thy t' [] nrandom size seed depth)))
           end
       | _ =>
           rpair NONE (fst (Predicate.yieldn k
-            (Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref)
+            (Code_Eval.eval NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
               Predicate.map thy t' [])))
   in ((T, ts), statistics) end;
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 10:45:22 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 12:16:08 2010 +0200
@@ -7,12 +7,15 @@
 signature PREDICATE_COMPILE_QUICKCHECK =
 sig
   (*val quickcheck : Proof.context -> term -> int -> term list option*)
-  val test_ref :
-    ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
-  val new_test_ref :
-    ((unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option) Unsynchronized.ref;
-  val eval_random_ref :
-    ((unit -> int -> int -> int -> int * int -> term list Predicate.pred) option) Unsynchronized.ref;
+  val put_pred_result :
+    (unit -> int -> int -> int -> int * int -> term list Predicate.pred) ->
+      Proof.context -> Proof.context;
+  val put_dseq_result :
+    (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) ->
+      Proof.context -> Proof.context;
+  val put_lseq_result :
+    (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) ->
+      Proof.context -> Proof.context;
 
   val tracing : bool Unsynchronized.ref;
   val quiet : bool Unsynchronized.ref;
@@ -30,15 +33,23 @@
 
 open Predicate_Compile_Aux;
 
-val test_ref =
-  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option);
+structure Pred_Result = Proof_Data (
+  type T = unit -> int -> int -> int -> int * int -> term list Predicate.pred
+  fun init _ () = error "Pred_Result"
+);
+val put_pred_result = Pred_Result.put;
 
-val new_test_ref =
-  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option)
+structure Dseq_Result = Proof_Data (
+  type T = unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)
+  fun init _ () = error "Dseq_Result"
+);
+val put_dseq_result = Dseq_Result.put;
 
-val eval_random_ref =
-  Unsynchronized.ref (NONE : (unit -> int -> int -> int -> int * int -> term list Predicate.pred) option);
-
+structure Lseq_Result = Proof_Data (
+  type T = unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence
+  fun init _ () = error "Lseq_Result"
+);
+val put_lseq_result = Lseq_Result.put;
 
 val tracing = Unsynchronized.ref false;
 
@@ -261,7 +272,7 @@
         Pos_Random_DSeq =>
           let
             val compiled_term =
-              Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
+              Code_Eval.eval (SOME target) (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
                 (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
                 thy4 qc_term []
           in
@@ -273,7 +284,7 @@
           let
             val compiled_term =
               Code_Eval.eval (SOME target)
-                ("Predicate_Compile_Quickcheck.new_test_ref", new_test_ref)
+                (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
                 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
                   g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
                   thy4 qc_term []
@@ -287,7 +298,7 @@
       | Depth_Limited_Random =>
           let
             val compiled_term = Code_Eval.eval (SOME target)
-              ("Predicate_Compile_Quickcheck.eval_random_ref", eval_random_ref)
+              (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
                 (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
                   g depth nrandom size seed |> (Predicate.map o map) proc)
                 thy4 qc_term []

--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Sep 15 10:45:22 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Sep 15 12:16:08 2010 +0200
@@ -15,9 +15,10 @@
   val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
   val compile_generator_expr:
     Proof.context -> term -> int -> term list option * (bool list * bool)
-  val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref
-  val eval_report_ref:
-    (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref
+  val put_counterexample: (unit -> int -> seed -> term list option * seed)
+    -> Proof.context -> Proof.context
+  val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
+    -> Proof.context -> Proof.context
   val setup: theory -> theory
 end;
 
@@ -304,13 +305,17 @@
 
 (** building and compiling generator expressions **)
 
-val eval_ref :
-    (unit -> int -> int * int -> term list option * (int * int)) option Unsynchronized.ref =
-  Unsynchronized.ref NONE;
+structure Counterexample = Proof_Data (
+  type T = unit -> int -> int * int -> term list option * (int * int)
+  fun init _ () = error "Counterexample"
+);
+val put_counterexample = Counterexample.put;
 
-val eval_report_ref :
-    (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref =
-  Unsynchronized.ref NONE;
+structure Counterexample_Report = Proof_Data (
+  type T = unit -> int -> seed -> (term list option * (bool list * bool)) * seed
+  fun init _ () = error "Counterexample_Report"
+);
+val put_counterexample_report = Counterexample_Report.put;
 
 val target = "Quickcheck";
 
@@ -387,13 +392,15 @@
   in if Quickcheck.report ctxt then
     let
       val t' = mk_reporting_generator_expr thy t Ts;
-      val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
+      val compile = Code_Eval.eval (SOME target)
+        (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
         (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) thy t' [];
     in compile #> Random_Engine.run end
   else
     let
       val t' = mk_generator_expr thy t Ts;
-      val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
+      val compile = Code_Eval.eval (SOME target)
+        (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
         (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
       val dummy_report = ([], false)
     in compile #> Random_Engine.run #> rpair dummy_report end

--- a/src/Pure/ML/ml_context.ML	Wed Sep 15 10:45:22 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Wed Sep 15 12:16:08 2010 +0200
@@ -36,8 +36,9 @@
   val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
   val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
     Context.generic -> Context.generic
-  val evaluate: Proof.context -> bool ->
-    string * (unit -> 'a) option Unsynchronized.ref -> string * string -> 'a
+  val value: Proof.context ->
+    (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
+    string * string -> 'a
 end
 
 structure ML_Context: ML_CONTEXT =
@@ -213,17 +214,15 @@
     (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
       ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
 
-
-(* FIXME not thread-safe -- reference can be accessed directly *)
-fun evaluate ctxt verbose (ref_name, r) (prelude, txt) = NAMED_CRITICAL "ML" (fn () =>
+fun value ctxt (get, put, put_ml) (prelude, value) =
   let
-    val s = prelude ^ "val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"
-    val ants = ML_Lex.read Position.none s;
-    val _ = r := NONE;
-    val _ =
-      Context.setmp_thread_data (SOME (Context.Proof ctxt))
-        (fn () => eval verbose Position.none ants) ();
-  in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
+    val read = ML_Lex.read Position.none;
+    val ants = read prelude @ read ("val _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
+      ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
+    val ctxt' = ctxt
+      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
+      |> Context.proof_map (exec (fn () => eval false Position.none ants));
+  in get ctxt' () end;
 
 end;
 

--- a/src/Tools/Code/code_eval.ML	Wed Sep 15 10:45:22 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Wed Sep 15 12:16:08 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;
 
 

--- a/src/Tools/nbe.ML	Wed Sep 15 10:45:22 2010 +0200
+++ b/src/Tools/nbe.ML	Wed Sep 15 12:16:08 2010 +0200
@@ -19,7 +19,7 @@
                                              (*abstractions as closures*)
   val same: Univ -> Univ -> bool
 
-  val univs_ref: (unit -> Univ list -> Univ list) option Unsynchronized.ref
+  val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
   val trace: bool Unsynchronized.ref
 
   val setup: theory -> theory
@@ -228,10 +228,15 @@
 
 (* nbe specific syntax and sandbox communication *)
 
-val univs_ref = Unsynchronized.ref (NONE : (unit -> Univ list -> Univ list) option);
+structure Univs = Proof_Data(
+  type T = unit -> Univ list -> Univ list
+  fun init thy () = error "Univs"
+);
+val put_result = Univs.put;
 
 local
   val prefix =      "Nbe.";
+  val name_put =    prefix ^ "put_result";
   val name_ref =    prefix ^ "univs_ref";
   val name_const =  prefix ^ "Const";
   val name_abss =   prefix ^ "abss";
@@ -239,7 +244,7 @@
   val name_same =   prefix ^ "same";
 in
 
-val univs_cookie = (name_ref, univs_ref);
+val univs_cookie = (Univs.get, put_result, name_put);
 
 fun nbe_fun 0 "" = "nbe_value"
   | nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i;
@@ -389,7 +394,7 @@
         s
         |> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
         |> pair ""
-        |> ML_Context.evaluate ctxt (!trace) univs_cookie
+        |> ML_Context.value ctxt univs_cookie
         |> (fn f => f deps_vals)
         |> (fn univs => cs ~~ univs)
       end;