diff -r 36df922b82d4 -r f7cdde18aeb3 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Aug 06 00:12:02 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Wed Aug 06 00:12:21 2008 +0200
@@ -148,7 +148,7 @@
 fun eval_antiquote lex node (str, pos) =
   let
     fun expand (Antiquote.Text s) = s
-      | expand (Antiquote.Antiq x) =
+      | expand (Antiquote.Antiq (x, _)) =
           let val (opts, src) = Antiquote.scan_arguments lex antiq x in
             options opts (fn () => command src node) ();  (*preview errors!*)
             PrintMode.with_modes (! modes @ Latex.modes)