diff -r 3bd1aa2f3517 -r 686a7d71ed7b src/Doc/Implementation/Logic.thy
--- 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