--- a/src/Doc/Implementation/Logic.thy Tue Apr 18 11:58:12 2023 +0200
+++ b/src/Doc/Implementation/Logic.thy Tue Apr 18 12:04:41 2023 +0200
@@ -701,7 +701,7 @@
\begin{mldecls}
@{define_ML Theory.add_deps: "Defs.context -> string ->
Defs.entry -> Defs.entry list -> theory -> theory"} \\
- @{define_ML Thm_Deps.all_oracles: "thm list -> Oracles.T"} \\
+ @{define_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\
\end{mldecls}
\<^descr> \<^ML>\<open>Logic.all\<close>~\<open>a B\<close> produces a Pure quantification \<open>\<And>a. B\<close>, where