added update_thy_only;
moved update_thy;

--- a/doc-src/Ref/introduction.tex	Fri Jul 30 15:40:54 1999 +0200
+++ b/doc-src/Ref/introduction.tex	Fri Jul 30 15:56:33 1999 +0200
@@ -169,6 +169,7 @@
 theory       : string -> theory
 use_thy      : string -> unit
 time_use_thy : string -> unit
+update_thy   : string -> unit
 \end{ttbox}
 
 \begin{ttdescription}
@@ -193,6 +194,11 @@
 \item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
   reports the time taken to process the actual theory parts and {\ML} files
   separately.
+
+\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
+  ensures that theory $name$ is fully up-to-date with respect to the file
+  system --- apart from $name$ itself any of its ancestors may be reloaded as
+  well.
   
 \end{ttdescription}
 

--- a/doc-src/Ref/theories.tex	Fri Jul 30 15:40:54 1999 +0200
+++ b/doc-src/Ref/theories.tex	Fri Jul 30 15:56:33 1999 +0200
@@ -246,7 +246,7 @@
 
 \begin{ttbox}
 use_thy_only    : string -> unit
-update_thy      : string -> unit
+update_thy_only : string -> unit
 touch_thy       : string -> unit
 remove_thy      : string -> unit
 delete_tmpfiles : bool ref \hfill{\bf initially true}
@@ -258,11 +258,10 @@
   $name$\texttt{.ML}.  This might be useful in replaying proof scripts by hand
   from the very beginning, starting with the fresh theory.
   
-\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
-  ensures that theory $name$ is fully up-to-date with respect to the file
-  system --- apart from $name$ itself any of its ancestors may be reloaded as
-  well.
-  
+\item[\ttindexbold{update_thy_only} "$name$";] is similar to
+  \texttt{update_thy}, but processes the actual theory file
+  $name$\texttt{.thy} only, ignoring $name$\texttt{.ML}.
+
 \item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the
   internal graph as outdated.  While the theory remains usable, subsequent
   operations such as \texttt{use_thy} may cause a reload.
@@ -308,10 +307,10 @@
 \end{ttdescription}
 
 In operations referring indirectly to some file, the argument may be prefixed
-by a directory that will be used as temporary load path, e.g.\ 
+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 care only.
+hard to predict.  Use this feature with great care only.
 
 
 \section{Locales}