1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun May 30 18:23:50 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun May 30 21:34:19 2010 +0200
     1.3 @@ -321,13 +321,13 @@
     1.4      (Keyword.tag_ml Keyword.thy_decl)
     1.5      (Parse.ML_source >> (fn (txt, pos) =>
     1.6        Toplevel.generic_theory
     1.7 -        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
     1.8 +        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #> propagate_env)));
     1.9  
    1.10  val _ =
    1.11    Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
    1.12      (Parse.ML_source >> (fn (txt, pos) =>
    1.13        Toplevel.proof (Proof.map_context (Context.proof_map
    1.14 -        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)));
    1.15 +        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)));
    1.16  
    1.17  val _ =
    1.18    Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)