| changeset 17218 | 64242b791c19 |
| parent 17186 | 797433ca1ab3 |
| child 19265 | cae36e16f3c0 |
--- a/src/Pure/Thy/latex.ML Thu Sep 01 15:58:08 2005 +0200 +++ b/src/Pure/Thy/latex.ML Thu Sep 01 15:58:10 2005 +0200 @@ -154,7 +154,7 @@ (* print mode *) val latexN = "latex"; -val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN]; +val modes = [latexN, Symbol.xsymbolsN]; fun latex_output str = let val syms = Symbol.explode str