1.1 --- a/src/Doc/IsarRef/Generic.thy	Sun Nov 11 20:47:04 2012 +0100
     1.2 +++ b/src/Doc/IsarRef/Generic.thy	Sun Nov 11 21:08:11 2012 +0100
     1.3 @@ -1976,4 +1976,49 @@
     1.4    \end{description}
     1.5  *}
     1.6  
     1.7 +
     1.8 +section {* Tracing higher-order unification *}
     1.9 +
    1.10 +text {*
    1.11 +  \begin{tabular}{rcll}
    1.12 +    @{attribute_def unify_trace_simp} & : & @{text "attribute"} & default @{text "false"} \\
    1.13 +    @{attribute_def unify_trace_types} & : & @{text "attribute"} & default @{text "false"} \\
    1.14 +    @{attribute_def unify_trace_bound} & : & @{text "attribute"} & default @{text "50"} \\
    1.15 +    @{attribute_def unify_search_bound} & : & @{text "attribute"} & default @{text "60"} \\
    1.16 +  \end{tabular}
    1.17 +  \medskip
    1.18 +
    1.19 +  Higher-order unification works well in most practical situations,
    1.20 +  but sometimes needs extra care to identify problems.  These tracing
    1.21 +  options may help.
    1.22 +
    1.23 +  \begin{description}
    1.24 +
    1.25 +  \item @{attribute unify_trace_simp} controls tracing of the
    1.26 +  simplification phase of higher-order unification.
    1.27 +
    1.28 +  \item @{attribute unify_trace_types} controls warnings of
    1.29 +  incompleteness, when unification is not considering all possible
    1.30 +  instantiations of schematic type variables.
    1.31 +
    1.32 +  \item @{attribute unify_trace_bound} determines the depth where
    1.33 +  unification starts to print tracing information once it reaches
    1.34 +  depth; 0 for full tracing.  At the default value, tracing
    1.35 +  information is almost never printed in practice.
    1.36 +
    1.37 +  \item @{attribute unify_search_bound} prevents unification from
    1.38 +  searching past the given depth.  Because of this bound, higher-order
    1.39 +  unification cannot return an infinite sequence, though it can return
    1.40 +  an exponentially long one.  The search rarely approaches the default
    1.41 +  value in practice.  If the search is cut off, unification prints a
    1.42 +  warning ``Unification bound exceeded''.
    1.43 +
    1.44 +  \end{description}
    1.45 +
    1.46 +  \begin{warn}
    1.47 +  Options for unification cannot be modified in a local context.  Only
    1.48 +  the global theory content is taken into account.
    1.49 +  \end{warn}
    1.50 +*}
    1.51 +
    1.52  end

     2.1 --- a/src/Doc/Ref/document/thm.tex	Sun Nov 11 20:47:04 2012 +0100
     2.2 +++ b/src/Doc/Ref/document/thm.tex	Sun Nov 11 21:08:11 2012 +0100
     2.3 @@ -46,39 +46,6 @@
     2.4  \end{ttdescription}
     2.5  
     2.6  
     2.7 -\subsection{Tracing flags for unification}
     2.8 -
     2.9 -\begin{ttbox} 
    2.10 -Unify.trace_simp   : bool ref \hfill\textbf{initially false}
    2.11 -Unify.trace_types  : bool ref \hfill\textbf{initially false}
    2.12 -Unify.trace_bound  : int ref \hfill\textbf{initially 10}
    2.13 -Unify.search_bound : int ref \hfill\textbf{initially 20}
    2.14 -\end{ttbox}
    2.15 -Tracing the search may be useful when higher-order unification behaves
    2.16 -unexpectedly.  Letting {\tt res_inst_tac} circumvent the problem is easier,
    2.17 -though.
    2.18 -\begin{ttdescription}
    2.19 -\item[set Unify.trace_simp;] 
    2.20 -causes tracing of the simplification phase.
    2.21 -
    2.22 -\item[set Unify.trace_types;] 
    2.23 -generates warnings of incompleteness, when unification is not considering
    2.24 -all possible instantiations of type unknowns.
    2.25 -
    2.26 -\item[Unify.trace_bound := $n$;] 
    2.27 -causes unification to print tracing information once it reaches depth~$n$.
    2.28 -Use $n=0$ for full tracing.  At the default value of~10, tracing
    2.29 -information is almost never printed.
    2.30 -
    2.31 -\item[Unify.search_bound := $n$;] prevents unification from
    2.32 -  searching past the depth~$n$.  Because of this bound, higher-order
    2.33 -  unification cannot return an infinite sequence, though it can return
    2.34 -  an exponentially long one.  The search rarely approaches the default value
    2.35 -  of~20.  If the search is cut off, unification prints a warning
    2.36 -  \texttt{Unification bound exceeded}.
    2.37 -\end{ttdescription}
    2.38 -
    2.39 -
    2.40  \section{*Primitive meta-level inference rules}
    2.41  
    2.42  \subsection{Logical equivalence rules}