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