'name' syntax includes numbers;

--- a/doc-src/IsarRef/syntax.tex	Wed Jan 26 11:04:38 2000 +0100
+++ b/doc-src/IsarRef/syntax.tex	Wed Jan 26 21:10:27 2000 +0100
@@ -101,7 +101,7 @@
 
 \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
 \begin{rail}
-  name: ident | symident | string
+  name: ident | symident | string | nat
   ;
   parname: '(' name ')'
   ;