--- a/doc-src/Ref/thm.tex Thu Jul 06 10:10:50 2000 +0200
+++ b/doc-src/Ref/thm.tex Thu Jul 06 11:23:39 2000 +0200
@@ -608,8 +608,9 @@
$\phi[\Var{x@k}/x]$. Thus, it replaces the outermost $\Forall$-bound
variable by an unknown having subscript~$k$.
-\item[\ttindexbold{forall_elim_vars} $ks$ $thm$]
-applies {\tt forall_elim_var} repeatedly, for every element of the list~$ks$.
+\item[\ttindexbold{forall_elim_vars} $k$ $thm$]
+applies {\tt forall_elim_var}~$k$ repeatedly until the theorem no longer has
+the form $\Forall x.\phi$.
\end{ttdescription}