src/Pure/Thy/latex.ML
changeset 58861 5ff61774df11
parent 58727 e3d0a6a012eb
child 58870 e2c0d8ef29cb
--- 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