--- 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) =
--- 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))) ()