--- a/src/Pure/Thy/latex.ML Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Thy/latex.ML Sat Nov 01 15:01:41 2014 +0100
@@ -119,11 +119,9 @@
(* token output *)
-val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment;
-
fun output_basic tok =
let val s = Token.content_of tok in
- if invisible_token tok then ""
+ if Token.is_kind Token.Comment tok then ""
else if Token.is_command tok then
"\\isacommand{" ^ output_syms s ^ "}"
else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then