diff -r c7f7cb82fd56 -r 68619606c5d1 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Mon Mar 27 18:09:24 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex	Mon Mar 27 18:09:49 2000 +0200
@@ -172,7 +172,7 @@
 \begin{rail}
   type: nameref | typefree | typevar
   ;
-  term: nameref | var | nat
+  term: nameref | var
   ;
   prop: term
   ;