src/Pure/Thy/latex.ML
changeset 14680 6029e76841fd
parent 14598 7009f59711e3
child 14840 dc23ff2629e2
     1.1 --- a/src/Pure/Thy/latex.ML	Mon Apr 26 15:00:20 2004 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Mon Apr 26 15:01:05 2004 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4          if invisible_token tok then ""
     1.5          else if T.is_kind T.Command tok then
     1.6            "\\isacommand{" ^ output_syms s ^ "}"
     1.7 -        else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
     1.8 +        else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
     1.9            "\\isakeyword{" ^ output_syms s ^ "}"
    1.10          else if T.is_kind T.String tok then output_syms (Library.quote s)
    1.11          else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)