# HG changeset patch
# User haftmann
# Date 1285832718 -7200
# Node ID b5f978f97347cfd2ad867d56725ecca8b6db162f
# Parent  9e59b4c11039d9dd38c8e0e256065eb3969f5ada
value uses bare compiler invocation: generated code does not contain antiquotations

diff -r 9e59b4c11039 -r b5f978f97347 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Sep 30 09:31:07 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Sep 30 09:45:18 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;