diff -r 39b931e00ba9 -r a32700e45ab3 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Thu Mar 05 18:19:20 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Thu Mar 05 19:48:02 2009 +0100
@@ -556,7 +556,7 @@
   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
   @{index_ML Thm.axiom: "theory -> string -> thm"} \\
-  @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
+  @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory
   -> (string * ('a -> thm)) * theory"} \\
   \end{mldecls}
   \begin{mldecls}
@@ -613,7 +613,7 @@
   \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named
   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
 
-  \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
+  \item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named
   oracle rule, essentially generating arbitrary axioms on the fly,
   cf.\ @{text "axiom"} in \figref{fig:prim-rules}.