# HG changeset patch
# User wenzelm
# Date 1352664491 -3600
# Node ID 01605e79c569227bfaa805036d33503e4b52ca24
# Parent  a025340c4abb17d654d48465fee3adfaf7f3bfe9
updated unification options;

diff -r a025340c4abb -r 01605e79c569 src/Doc/IsarRef/Generic.thy
--- a/src/Doc/IsarRef/Generic.thy	Sun Nov 11 20:47:04 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy	Sun Nov 11 21:08:11 2012 +0100
@@ -1976,4 +1976,49 @@
   \end{description}
 *}
 
+
+section {* Tracing higher-order unification *}
+
+text {*
+  \begin{tabular}{rcll}
+    @{attribute_def unify_trace_simp} & : & @{text "attribute"} & default @{text "false"} \\
+    @{attribute_def unify_trace_types} & : & @{text "attribute"} & default @{text "false"} \\
+    @{attribute_def unify_trace_bound} & : & @{text "attribute"} & default @{text "50"} \\
+    @{attribute_def unify_search_bound} & : & @{text "attribute"} & default @{text "60"} \\
+  \end{tabular}
+  \medskip
+
+  Higher-order unification works well in most practical situations,
+  but sometimes needs extra care to identify problems.  These tracing
+  options may help.
+
+  \begin{description}
+
+  \item @{attribute unify_trace_simp} controls tracing of the
+  simplification phase of higher-order unification.
+
+  \item @{attribute unify_trace_types} controls warnings of
+  incompleteness, when unification is not considering all possible
+  instantiations of schematic type variables.
+
+  \item @{attribute unify_trace_bound} determines the depth where
+  unification starts to print tracing information once it reaches
+  depth; 0 for full tracing.  At the default value, tracing
+  information is almost never printed in practice.
+
+  \item @{attribute unify_search_bound} prevents unification from
+  searching past the given depth.  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 in practice.  If the search is cut off, unification prints a
+  warning ``Unification bound exceeded''.
+
+  \end{description}
+
+  \begin{warn}
+  Options for unification cannot be modified in a local context.  Only
+  the global theory content is taken into account.
+  \end{warn}
+*}
+
 end
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}