changeset 61505 | a4478ca660a5 |
parent 61475 | 5b58a17c440a |
child 61516 | 8e3705d91cfa |
--- 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);