src/Pure/Thy/latex.ML
changeset 27771 98499933a50f
parent 27755 f7cdde18aeb3
child 27781 5a82ee34e9fc
     1.1 --- a/src/Pure/Thy/latex.ML	Thu Aug 07 13:45:07 2008 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Thu Aug 07 13:45:09 2008 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4  val output_syms = output_symbols o Symbol.explode;
     1.5  
     1.6  val output_syms_antiqs =
     1.7 -  Antiquote.scan_antiquotes #> map
     1.8 +  Antiquote.read #> map
     1.9    (fn Antiquote.Text s => output_syms s
    1.10      | Antiquote.Antiq ((s, _), _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
    1.11      | Antiquote.Open _ => "{\\isaantiqopen}"