src/Pure/Thy/latex.ML
changeset 28375 c879d88d038a
parent 27885 76b51cd0a37c
child 29325 a205acc94356
     1.1 --- a/src/Pure/Thy/latex.ML	Fri Sep 26 17:24:15 2008 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Fri Sep 26 19:07:56 2008 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4  
     1.5  structure T = OuterLex;
     1.6  
     1.7 -val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
     1.8 +val invisible_token = T.keyword_with (fn s => s = ";") orf T.is_kind T.Comment;
     1.9  
    1.10  fun output_basic tok =
    1.11    let val s = T.content_of tok in