tuned;

--- a/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 21:13:06 2000 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 21:13:23 2000 +0200
@@ -11,6 +11,7 @@
 
 \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
+\railterm{name,nameref,text,type,term,prop,atom}
 
 \railalias{ident}{\railtoken{ident}}
 \railalias{longident}{\railtoken{longident}}