diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/Thy/latex.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -102,7 +102,7 @@
 
 structure T = OuterLex;
 
-val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
+val invisible_token = T.keyword_with (fn s => s = ";") orf T.is_kind T.Comment;
 
 fun output_basic tok =
   let val s = T.content_of tok in