diff -r 4cc2b6046258 -r c49b328d689d doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Sep 18 19:39:44 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Sep 18 19:39:47 2008 +0200
@@ -593,12 +593,12 @@
   \indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
   \indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
   \indexml{Thm.get\_axiom\_i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
-  \indexml{Thm.invoke\_oracle\_i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
+  \indexml{Thm.add\_oracle}\verb|Thm.add_oracle: bstring * ('a -> cterm) -> theory|\isasep\isanewline%
+\verb|  -> (string * ('a -> thm)) * theory| \\
   \end{mldecls}
   \begin{mldecls}
   \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
   \indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
-  \indexml{Theory.add\_oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
   \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
   \end{mldecls}
 
@@ -646,16 +646,13 @@
   \item \verb|Thm.get_axiom_i|~\isa{thy\ name} retrieves a named
   axiom, cf.\ \isa{axiom} in \figref{fig:prim-rules}.
 
-  \item \verb|Thm.invoke_oracle_i|~\isa{thy\ name\ arg} invokes a
-  named oracle function, cf.\ \isa{axiom} in
-  \figref{fig:prim-rules}.
+  \item \verb|Thm.add_oracle|~\isa{{\isacharparenleft}name{\isacharcomma}\ oracle{\isacharparenright}} produces a named
+  oracle rule, essentially generating arbitrary axioms on the fly,
+  cf.\ \isa{axiom} in \figref{fig:prim-rules}.
 
   \item \verb|Theory.add_axioms_i|~\isa{{\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares
   arbitrary propositions as axioms.
 
-  \item \verb|Theory.add_oracle|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}} declares an oracle
-  function for generating arbitrary axioms on the fly.
-
   \item \verb|Theory.add_deps|~\isa{name\ c\isactrlisub {\isasymtau}\ \isactrlvec d\isactrlisub {\isasymsigma}} declares dependencies of a named specification
   for constant \isa{c\isactrlisub {\isasymtau}}, relative to existing
   specifications for constants \isa{\isactrlvec d\isactrlisub {\isasymsigma}}.