--- a/src/Doc/Logics/document/HOL.tex Wed Feb 28 23:50:22 2024 +0100
+++ b/src/Doc/Logics/document/HOL.tex Wed Feb 28 15:19:15 2024 +0100
@@ -177,7 +177,7 @@
guarantee to find instantiations for type variables automatically. Be
prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},
possibly instantiating type variables. Setting
- \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report
+ \ttindex{Unify.unify_trace_types} to \texttt{true} causes Isabelle to report
omitted search paths during unification.\index{tracing!of unification}
\end{warn}