--- a/doc-src/Ref/theories.tex Sun Feb 04 19:40:54 2001 +0100
+++ b/doc-src/Ref/theories.tex Sun Feb 04 19:41:30 2001 +0100
@@ -291,6 +291,7 @@
del_path: string -> unit
reset_path: unit -> unit
with_path: string -> ('a -> 'b) -> 'a -> 'b
+no_document: ('a -> 'b) -> 'a -> 'b
\end{ttbox}
\begin{ttdescription}
@@ -307,7 +308,10 @@
(current directory) only.
\item[\ttindexbold{with_path} "$dir$" $f$ $x$;] temporarily adds component
- $dir$ to the beginning of the load path before executing $(f~x)$.
+ $dir$ to the beginning of the load path while executing $(f~x)$.
+
+\item[\ttindexbold{no_document} $f$ $x$;] temporarily disables {\LaTeX}
+ document generation while executing $(f~x)$.
\end{ttdescription}