diff -r 10d84e124a2f -r 98499933a50f src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Aug 07 13:45:07 2008 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Aug 07 13:45:09 2008 +0200
@@ -89,7 +89,7 @@
 val output_syms = output_symbols o Symbol.explode;
 
 val output_syms_antiqs =
-  Antiquote.scan_antiquotes #> map
+  Antiquote.read #> map
   (fn Antiquote.Text s => output_syms s
     | Antiquote.Antiq ((s, _), _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
     | Antiquote.Open _ => "{\\isaantiqopen}"