# HG changeset patch
# User wenzelm
# Date 1413837977 -7200
# Node ID e3d0a6a012eb05c287df4fc7817eb85e318739aa
# Parent  cee57ab1f76f367dcc726a4774a9919a45d71f45
avoid odd ligatures;

diff -r cee57ab1f76f -r e3d0a6a012eb src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Oct 20 21:48:03 2014 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Oct 20 22:46:17 2014 +0200
@@ -39,7 +39,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);