# HG changeset patch
# User wenzelm
# Date 1445546288 -7200
# Node ID a4478ca660a54cf65dee5a1990ef96d6a049cd87
# Parent  a7ae3ef886a9a635879e9269eae78dd8b8451c41
more robust ASCII output: avoid ligatures of quotes;

diff -r a7ae3ef886a9 -r a4478ca660a5 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Oct 22 21:34:28 2015 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Oct 22 22:38:08 2015 +0200
@@ -36,7 +36,7 @@
       | "\t" => "\\ "
       | "\n" => "\\isanewline\n"
       | s =>
-          if exists_string (fn s' => s = s') "#$%^&_{}~\\<>"
+          if exists_string (fn s' => s = s') "\"#$%&'<>\\^_{}~"
           then enclose "{\\char`\\" "}" s else s);