diff -r caa7a52ff46f -r 919a03a587eb doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Thu Nov 25 14:23:04 1993 +0100
+++ b/doc-src/Ref/theories.tex	Thu Nov 25 14:32:54 1993 +0100
@@ -173,25 +173,21 @@
 \label{LoadingTheories}
 \subsection{Reading a new theory}
 
-\begin{ttbox} 
-use_thy: string -> unit
-\end{ttbox}
 Each theory definition must reside in a separate file.  Let the file {\it
   tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
 theories $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"}{\it
   TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file
-{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file.  Any of the parent
-theories that have not been loaded yet are read now by recursive {\tt
-  use_thy} calls until either an already loaded theory or {\tt Pure} is
-reached.  Therefore one can read a complete logic by just one {\tt use_thy}
-call if all theories are linked appropriatly.  Afterwards an {\ML}
+{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. \indexbold{automatic
+loading}  Any of the parent theories that have not been loaded yet are read now
+by recursive {\tt use_thy} calls until either an already loaded theory or {\tt
+  Pure} is reached.  Therefore one can read a complete logic by just one {\tt
+use_thy} call if all theories are linked appropriatly.  Afterwards an {\ML}
 structure~$TF$ containing a component {\tt thy} for the new theory and
 components $r@1$ \dots $r@n$ for the rules is declared; it also contains the
 definitions of the {\tt ML} section if any. Unless
-\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it
-  tf}{\tt.thy.ML} is deleted if no errors occured. Finally the file {\it
-  tf}{\tt.ML} is read, if it exists; this file normally contains proofs
-involving the new theory.
+\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it tf}{\tt.thy.ML}
+is deleted if no errors occured. Finally the file {\it tf}{\tt.ML} is read, if
+it exists; this file normally contains proofs involving the new theory.
 
 
 \subsection{Filenames and paths}