diff -r e89fd7d0a624 -r b4dcc32310fb doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Mon Aug 23 15:24:00 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex	Mon Aug 23 15:27:27 1999 +0200
@@ -134,7 +134,7 @@
 \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
 \indexouternonterm{classdecl}
 \begin{rail}
-  classdecl: name ('<' (nameref ',' +))?
+  classdecl: name ('<' (nameref + ','))?
   ;
   sort: nameref | lbrace (nameref * ',') rbrace
   ;