src/Pure/Thy/latex.ML
changeset 8896 c80aba8c1d5e
parent 8808 204f4ebbba64
child 8965 d46b36785c70
     1.1 --- a/src/Pure/Thy/latex.ML	Sun May 21 14:32:47 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Sun May 21 14:33:46 2000 +0200
     1.3 @@ -76,8 +76,8 @@
     1.4        let val s = T.val_of tok in
     1.5          if invisible_token tok then ""
     1.6          else if T.is_kind T.Command tok then
     1.7 -          if s = "{{" then "{\\isabeginblock}"
     1.8 -          else if s = "}}" then "{\\isaendblock}"
     1.9 +          if s = "{" then "{\\isabeginblock}"
    1.10 +          else if s = "}" then "{\\isaendblock}"
    1.11            else "\\isacommand{" ^ output_syms s ^ "}"
    1.12          else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
    1.13            "\\isakeyword{" ^ output_syms s ^ "}"