src/Pure/Thy/latex.ML
changeset 30589 cbe27c4ef417
parent 30573 49899f26fbd1
child 30590 1d9c9fcf8513
     1.1 --- a/src/Pure/Thy/latex.ML	Thu Mar 19 15:22:53 2009 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Thu Mar 19 15:44:14 2009 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4  val output_syms = output_symbols o Symbol.explode;
     1.5  
     1.6  val output_syms_antiq =
     1.7 -  (fn Antiquote.Text s => output_syms s
     1.8 +  (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
     1.9      | Antiquote.Antiq (ss, _) =>
    1.10          enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
    1.11      | Antiquote.Open _ => "{\\isaantiqopen}"