diff -r a025340c4abb -r 01605e79c569 src/Doc/Ref/document/thm.tex
--- a/src/Doc/Ref/document/thm.tex	Sun Nov 11 20:47:04 2012 +0100
+++ b/src/Doc/Ref/document/thm.tex	Sun Nov 11 21:08:11 2012 +0100
@@ -46,39 +46,6 @@
 \end{ttdescription}
 
 
-\subsection{Tracing flags for unification}
-
-\begin{ttbox} 
-Unify.trace_simp   : bool ref \hfill\textbf{initially false}
-Unify.trace_types  : bool ref \hfill\textbf{initially false}
-Unify.trace_bound  : int ref \hfill\textbf{initially 10}
-Unify.search_bound : int ref \hfill\textbf{initially 20}
-\end{ttbox}
-Tracing the search may be useful when higher-order unification behaves
-unexpectedly.  Letting {\tt res_inst_tac} circumvent the problem is easier,
-though.
-\begin{ttdescription}
-\item[set Unify.trace_simp;] 
-causes tracing of the simplification phase.
-
-\item[set Unify.trace_types;] 
-generates warnings of incompleteness, when unification is not considering
-all possible instantiations of type unknowns.
-
-\item[Unify.trace_bound := $n$;] 
-causes unification to print tracing information once it reaches depth~$n$.
-Use $n=0$ for full tracing.  At the default value of~10, tracing
-information is almost never printed.
-
-\item[Unify.search_bound := $n$;] prevents unification from
-  searching past the depth~$n$.  Because of this bound, higher-order
-  unification cannot return an infinite sequence, though it can return
-  an exponentially long one.  The search rarely approaches the default value
-  of~20.  If the search is cut off, unification prints a warning
-  \texttt{Unification bound exceeded}.
-\end{ttdescription}
-
-
 \section{*Primitive meta-level inference rules}
 
 \subsection{Logical equivalence rules}