# HG changeset patch
# User wenzelm
# Date 1237751388 -3600
# Node ID 955830462054f27868ae92c08eb0680a008e112b
# Parent  0c9f9c49d5df5a15c78aa7965e7396423ae2ee31
ML_Lex.read_antiq;

diff -r 0c9f9c49d5df -r 955830462054 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sun Mar 22 20:49:47 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Sun Mar 22 20:49:48 2009 +0100
@@ -240,8 +240,7 @@
 
     (*prepare source text*)
     val _ = Position.report Markup.ML_source pos;
-    val ants = (Symbol_Pos.explode (txt, pos), pos)
-      |> Antiquote.read ML_Lex.report_token ML_Lex.scan_antiq;
+    val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
     val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ())
       |>> pairself (implode o map ML_Lex.text_of);
     val _ = if ! trace then tracing (cat_lines [env, body]) else ();