--- a/src/Pure/Thy/latex.ML Tue Dec 02 17:30:53 2014 +0100
+++ b/src/Pure/Thy/latex.ML Wed Dec 03 11:37:51 2014 +0100
@@ -128,7 +128,7 @@
"\\isakeyword{" ^ output_syms s ^ "}"
else if Token.is_kind Token.String tok then
enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
- else if Token.is_kind Token.AltString tok then
+ else if Token.is_kind Token.Alt_String tok then
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
else if Token.is_kind Token.Verbatim tok then
let