1.1 --- a/src/Pure/ML/ml_context.ML	Thu Sep 30 09:31:07 2010 +0200
     1.2 +++ b/src/Pure/ML/ml_context.ML	Thu Sep 30 09:45:18 2010 +0200
     1.3 @@ -217,12 +217,13 @@
     1.4  
     1.5  fun value ctxt (get, put, put_ml) (prelude, value) =
     1.6    let
     1.7 -    val read = ML_Lex.read Position.none;
     1.8 -    val ants = read prelude @ read ("val _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
     1.9 +    val code = (prelude
    1.10 +      ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    1.11        ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
    1.12      val ctxt' = ctxt
    1.13        |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.14 -      |> Context.proof_map (exec (fn () => eval false Position.none ants));
    1.15 +      |> Context.proof_map (exec
    1.16 +          (fn () => Secure.use_text ML_Env.local_context (0, "value") false code));
    1.17    in get ctxt' () end;
    1.18  
    1.19  end;