doc-src/Ref/theories.tex

--- a/doc-src/Ref/theories.tex	Mon Jul 22 16:24:47 1996 +0200
+++ b/doc-src/Ref/theories.tex	Tue Jul 23 13:19:27 1996 +0200
@@ -935,7 +935,7 @@
 
 \begin{ttbox}
      invoke_oracle : theory * Sign.sg * exn -> thm
-     set_oracle    : Sign.sg -> typ -> string
+     set_oracle    : (Sign.sg * exn -> term) -> theory -> theory
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{invoke_oracle} ($thy$, $sign$, $exn$)] invokes the oracle