diff -r 4a04b6bd628b -r 910a081cca74 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Mon Feb 24 12:14:13 2020 +0000
+++ b/src/Doc/Implementation/Logic.thy	Mon Feb 24 20:57:29 2020 +0100
@@ -598,7 +598,7 @@
   \begin{mldecls}
   @{index_ML Theory.add_deps: "Defs.context -> string ->
   Defs.entry -> Defs.entry list -> theory -> theory"} \\
-  @{index_ML Thm_Deps.all_oracles: "thm list -> (string * term option) list"} \\
+  @{index_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
@@ -676,9 +676,10 @@
 
   \<^descr> \<^ML>\<open>Thm_Deps.all_oracles\<close>~\<open>thms\<close> returns all oracles used in the
   internal derivation of the given theorems; this covers the full graph of
-  transitive dependencies. The result contains a name, plus the original
-  proposition, if @{ML Proofterm.proofs} was at least @{ML 1} during the
-  oracle inference. See also the command @{command_ref "thm_oracles"}.
+  transitive dependencies. The result contains an authentic oracle name; if
+  @{ML Proofterm.proofs} was at least @{ML 1} during the oracle inference, it
+  also contains the position of the oracle invocation and its proposition. See
+  also the command @{command_ref "thm_oracles"}.
 \<close>
 
 text %mlantiq \<open>