# HG changeset patch
# User bulwahn
# Date 1285840342 -7200
# Node ID 3a7e2964c9c02d5513ee2ade5904e8487db4514c
# Parent  17e29ddd538e822ad12d352069a93871e68ef55c# Parent  b5f978f97347cfd2ad867d56725ecca8b6db162f
merged

diff -r 17e29ddd538e -r 3a7e2964c9c0 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Sep 30 10:48:12 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Sep 30 11:52:22 2010 +0200
@@ -217,12 +217,13 @@
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
   let
-    val read = ML_Lex.read Position.none;
-    val ants = read prelude @ read ("val _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
+    val code = (prelude
+      ^ "\nval _ = 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));
+      |> Context.proof_map (exec
+          (fn () => Secure.use_text ML_Env.local_context (0, "value") false code));
   in get ctxt' () end;
 
 end;