diff -r 19df8385f38d -r e87888b4152f doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Wed May 18 23:39:22 2011 +0200
+++ b/doc-src/Ref/theories.tex	Fri May 20 14:03:42 2011 +0200
@@ -2,52 +2,6 @@
 \chapter{Theories, Terms and Types} \label{theories}
 \index{theories|(}
 
-\section{The theory loader}\label{sec:more-theories}
-\index{theories!reading}\index{files!reading}
-
-Isabelle's theory loader manages dependencies of the internal graph of theory
-nodes (the \emph{theory database}) and the external view of the file system.
-
-\medskip Theory and {\ML} files are located by skimming through the
-directories listed in Isabelle's internal load path, which merely contains the
-current directory ``\texttt{.}'' by default.  The load path may be accessed by
-the following operations.
-
-\begin{ttbox}
-show_path: unit -> string list
-add_path: string -> unit
-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}
-\item[\ttindexbold{show_path}();] displays the load path components in
-  canonical string representation (which is always according to Unix rules).
-  
-\item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning
-  of the load path.
-  
-\item[\ttindexbold{del_path} "$dir$";] removes any occurrences of component
-  $dir$ from the load path.
-  
-\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 while executing $(f~x)$.
-  
-\item[\ttindexbold{no_document} $f$ $x$;] temporarily disables {\LaTeX}
-  document generation while executing $(f~x)$.
-
-\end{ttdescription}
-
-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{Basic operations on theories}\label{BasicOperationsOnTheories}
 
 \subsection{*Theory inclusion}