simplified Antiquote signature;

--- a/src/Pure/ML/ml_context.ML	Thu Aug 07 19:21:42 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Aug 07 19:21:43 2008 +0200
@@ -138,10 +138,10 @@
           fun no_decl _ = ("", "");
 
           fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state)
-            | expand (Antiquote.Antiq (x, _)) (scope, background) =
+            | expand (Antiquote.Antiq x) (scope, background) =
                 let
                   val context = Stack.top scope;
-                  val (f, context') = antiquotation (Antiquote.read_arguments lex antiq x) context;
+                  val (f, context') = antiquotation (Antiquote.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/latex.ML	Thu Aug 07 19:21:42 2008 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Aug 07 19:21:43 2008 +0200
@@ -87,11 +87,12 @@
 val output_known_symbols = implode oo (map o output_known_sym);
 val output_symbols = output_known_symbols (K true, K true);
 val output_syms = output_symbols o Symbol.explode;
+val output_syms' = output_symbols o map #1 o SymbolPos.explode;
 
 val output_syms_antiqs =
   Antiquote.read #> map
   (fn Antiquote.Text s => output_syms s
-    | Antiquote.Antiq ((s, _), _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
+    | Antiquote.Antiq x => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms' x)
     | Antiquote.Open _ => "{\\isaantiqopen}"
     | Antiquote.Close _ => "{\\isaantiqclose}") #>
   implode;

--- a/src/Pure/Thy/thy_output.ML	Thu Aug 07 19:21:42 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Aug 07 19:21:43 2008 +0200
@@ -148,8 +148,8 @@
 fun eval_antiquote lex node (str, pos) =
   let
     fun expand (Antiquote.Text s) = s
-      | expand (Antiquote.Antiq (x, _)) =
-          let val (opts, src) = Antiquote.read_arguments lex antiq x in
+      | expand (Antiquote.Antiq x) =
+          let val (opts, src) = Antiquote.read_antiq lex antiq x in
             options opts (fn () => command src node) ();  (*preview errors!*)
             PrintMode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings (options opts (fn () => command src node))) ()