diff -r 34f3ec8d4d24 -r c2535056434f src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Tue Oct 29 10:26:06 2024 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Oct 31 09:24:10 2024 +0100
@@ -630,6 +630,9 @@
 \item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}.
 \end{enum}
 
+The \textit{metis} method also supports the Isabelle option
+[[\textit{metis\_suggest\_of}]], which tells \textit{metis} to suggest
+instantiations of facts using \textbf{of} from a successful proof.
 
 \section{Option Reference}
 \label{option-reference}
@@ -1218,10 +1221,6 @@
 \textit{B}"]). This can make the proof methods faster and more intelligible. If
 the option is set to \textit{smart} (the default), variable instantiations are
 inferred only if proof reconstruction failed or timed out.
-
-When using \textit{metis} directly, enable the configuration
-option [[\textit{metis\_suggest\_of}]] to directly get a suggestion with
-instantiations of facts using \textbf{of} from a successful proof.
 \end{enum}