# HG changeset patch
# User wenzelm
# Date 936278640 -7200
# Node ID c1829208180f9dd94115406c123e9dec7d9f6bcc
# Parent  a1b3310b4985dfe3129fe67fcd84772950973165
added with_path;

diff -r a1b3310b4985 -r c1829208180f doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Thu Sep 02 15:23:05 1999 +0200
+++ b/doc-src/Ref/theories.tex	Thu Sep 02 15:24:00 1999 +0200
@@ -290,6 +290,7 @@
 add_path: string -> unit
 del_path: string -> unit
 reset_path: unit -> unit
+with_path: string -> ('a -> 'b) -> 'a -> 'b
 \end{ttbox}
 
 \begin{ttdescription}
@@ -304,13 +305,15 @@
   
 \item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}''
   (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)$.
+
 \end{ttdescription}
 
-In operations referring indirectly to some file, the argument may be prefixed
-by a directory that will be temporarily appended to the load path, e.g.\ 
-\texttt{use_thy~"$dir/name$"}.  Note that, depending on which parts of the
-ancestry of $name$ are already loaded, the dynamic change of paths might be
-hard to predict.  Use this feature with great care only.
+Furthermore, in operations referring indirectly to some file (e.g.\ 
+\texttt{use_dir}) the argument may be prefixed by a directory that will be
+temporarily appended to the load path, too.
 
 
 \section{Locales}