# HG changeset patch
# User wenzelm
# Date 1237472573 -3600
# Node ID 05f81bbb2614a95d1eff5a793d75f92d66dd4185
# Parent  ad19c99529eb6c3da943858e5414b1503aabeef6
OuterLex.read_antiq;

diff -r ad19c99529eb -r 05f81bbb2614 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 19 15:22:53 2009 +0100
@@ -183,6 +183,7 @@
 local
 
 structure P = OuterParse;
+structure T = OuterLex;
 
 val antiq =
   P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
@@ -213,7 +214,7 @@
             | expand (Antiquote.Antiq x) (scope, background) =
                 let
                   val context = Stack.top scope;
-                  val (f, context') = antiquotation (Antiquote.read_antiq lex antiq x) context;
+                  val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
                   val (decl, background') = f {background = background, struct_name = struct_name};
                 in (decl, (Stack.map_top (K context') scope, background')) end
             | expand (Antiquote.Open _) (scope, background) =
diff -r ad19c99529eb -r 05f81bbb2614 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 19 15:22:53 2009 +0100
@@ -149,7 +149,7 @@
   let
     fun expand (Antiquote.Text s) = s
       | expand (Antiquote.Antiq x) =
-          let val (opts, src) = Antiquote.read_antiq lex antiq x in
+          let val (opts, src) = T.read_antiq lex antiq x in
             options opts (fn () => command src state) ();  (*preview errors!*)
             PrintMode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings (options opts (fn () => command src state))) ()