diff -r 68619606c5d1 -r d2e2a3df6871 doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 18:09:49 2000 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 18:10:11 2000 +0200
@@ -12,6 +12,18 @@
 \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
 
+\railalias{ident}{\railtoken{ident}}
+\railalias{longident}{\railtoken{longident}}
+\railalias{symident}{\railtoken{symident}}
+\railalias{var}{\railtoken{var}}
+\railalias{textvar}{\railtoken{textvar}}
+\railalias{typefree}{\railtoken{typefree}}
+\railalias{typevar}{\railtoken{typevar}}
+\railalias{nat}{\railtoken{nat}}
+\railalias{string}{\railtoken{string}}
+\railalias{verbatim}{\railtoken{verbatim}}
+\railalias{keyword}{\railtoken{keyword}}
+
 \railalias{name}{\railqtoken{name}}
 \railalias{nameref}{\railqtoken{nameref}}
 \railalias{text}{\railqtoken{text}}