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

     2.1 --- a/doc-src/Ref/theories.tex	Fri Jul 30 15:40:54 1999 +0200
     2.2 +++ b/doc-src/Ref/theories.tex	Fri Jul 30 15:56:33 1999 +0200
     2.3 @@ -246,7 +246,7 @@
     2.4  
     2.5  \begin{ttbox}
     2.6  use_thy_only    : string -> unit
     2.7 -update_thy      : string -> unit
     2.8 +update_thy_only : string -> unit
     2.9  touch_thy       : string -> unit
    2.10  remove_thy      : string -> unit
    2.11  delete_tmpfiles : bool ref \hfill{\bf initially true}
    2.12 @@ -258,11 +258,10 @@
    2.13    $name$\texttt{.ML}.  This might be useful in replaying proof scripts by hand
    2.14    from the very beginning, starting with the fresh theory.
    2.15    
    2.16 -\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
    2.17 -  ensures that theory $name$ is fully up-to-date with respect to the file
    2.18 -  system --- apart from $name$ itself any of its ancestors may be reloaded as
    2.19 -  well.
    2.20 -  
    2.21 +\item[\ttindexbold{update_thy_only} "$name$";] is similar to
    2.22 +  \texttt{update_thy}, but processes the actual theory file
    2.23 +  $name$\texttt{.thy} only, ignoring $name$\texttt{.ML}.
    2.24 +
    2.25  \item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the
    2.26    internal graph as outdated.  While the theory remains usable, subsequent
    2.27    operations such as \texttt{use_thy} may cause a reload.
    2.28 @@ -308,10 +307,10 @@
    2.29  \end{ttdescription}
    2.30  
    2.31  In operations referring indirectly to some file, the argument may be prefixed
    2.32 -by a directory that will be used as temporary load path, e.g.\ 
    2.33 +by a directory that will be temporarily appended to the load path, e.g.\ 
    2.34  \texttt{use_thy~"$dir/name$"}.  Note that, depending on which parts of the
    2.35  ancestry of $name$ are already loaded, the dynamic change of paths might be
    2.36 -hard to predict.  Use this feature with care only.
    2.37 +hard to predict.  Use this feature with great care only.
    2.38  
    2.39  
    2.40  \section{Locales}