diff -r 37aa547fb564 -r fe7b812837ad doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Mon Sep 22 17:35:52 1997 +0200
+++ b/doc-src/Ref/defining.tex	Mon Sep 22 17:37:03 1997 +0200
@@ -104,10 +104,12 @@
       &$|$& $logic^{(4)}$ {\tt::} $type$ & (3) \\
       &$|$& $id$ ~~$|$~~ $var$
     ~~$|$~~ $logic^{(\infty)}$ {\tt(} $any$ {\tt,} \dots {\tt,} $any$ {\tt)} \\
-      &$|$& {\tt \%} $idts$ {\tt.} $any^{(3)}$ & (3) \\\\
+      &$|$& {\tt \%} $pttrns$ {\tt.} $any^{(3)}$ & (3) \\\\
 $idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
 $idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
     &$|$& $id$ {\tt ::} $type$ & (0) \\\\
+$pttrns$ &=& $pttrn$ ~~$|$~~ $pttrn^{(1)}$ $pttrns$ \\\\
+$pttrn$ &=& $idt$ \\\\
 $type$ &=& {\tt(} $type$ {\tt)} \\
      &$|$& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
        ~~$|$~~ $tvar$ {\tt::} $sort$ \\
@@ -164,6 +166,10 @@
 
   \item[\ndxbold{idts}] denotes a list of identifiers, possibly constrained
     by types.
+    
+  \item[\ndxbold{pttrn}, \ndxbold{pttrns}] denote patterns for
+    abstraction, cases etc.  Initially the same as $idt$ and $idts$,
+    these are indetended to be augmented by user extensions.
 
   \item[\ndxbold{type}] denotes types of the meta-logic.