src/Pure/Thy/latex.ML
changeset 66020 a31760eee09d
parent 64526 01920e390645
child 66021 08ab52fb9db5
     1.1 --- a/src/Pure/Thy/latex.ML	Mon Jun 05 23:55:58 2017 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Jun 06 13:13:25 2017 +0200
     1.3 @@ -206,7 +206,7 @@
     1.4  (* print mode *)
     1.5  
     1.6  val latexN = "latex";
     1.7 -val modes = [latexN, Symbol.xsymbolsN];
     1.8 +val modes = [latexN];
     1.9  
    1.10  fun latex_output str =
    1.11    let val syms = Symbol.explode str