# HG changeset patch
# User paulson
# Date 838120767 -7200
# Node ID 78c4b3ddba6cc31e5eb6ea6b65dd5d8d7a8689b2
# Parent  83c70ad381c14504b2354478faa79dd8fbca77f0
Corrected typo regarding the type of set_oracle

diff -r 83c70ad381c1 -r 78c4b3ddba6c 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