diff -r 2913a54e64cf -r c80aba8c1d5e doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Sun May 21 14:32:47 2000 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Sun May 21 14:33:46 2000 +0200
@@ -9,7 +9,7 @@
 
 \makeindex
 
-\railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
+\railterm{percent,ppercent,underscore}
 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
 \railterm{name,nameref,text,type,term,prop,atom}