1.1 --- a/doc-src/IsarRef/isar-ref.tex	Sun May 21 14:32:47 2000 +0200
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Sun May 21 14:33:46 2000 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  \makeindex
     1.6  
     1.7 -\railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
     1.8 +\railterm{percent,ppercent,underscore}
     1.9  \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
    1.10  \railterm{name,nameref,text,type,term,prop,atom}
    1.11