# HG changeset patch
# User wenzelm
# Date 1221759587 -7200
# Node ID c49b328d689dcc57ffb68d9f502560f6c858d78f
# Parent  4cc2b6046258168627a5a22efefa2bec4ce80bc9
updated generated file;

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}}.
diff -r 4cc2b6046258 -r c49b328d689d doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu Sep 18 19:39:44 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu Sep 18 19:39:47 2008 +0200
@@ -1135,8 +1135,8 @@
     \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isartrans{theory}{theory} \\
   \end{matharray}
 
-  The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some
-  type \verb|T| given by the user.  This acts like an infinitary
+  The oracle interface promotes a given ML function \verb|'a -> cterm|
+  to \verb|'a -> thm|.  This acts like an infinitary
   specification of axioms -- there is no internal check of the
   correctness of the results!  The inference kernel records oracle
   invocations within the internal derivation object of theorems, and
@@ -1144,18 +1144,16 @@
   that are not fully checked by Isabelle inferences.
 
   \begin{rail}
-    'oracle' name '(' type ')' '=' text
+    'oracle' name '=' text
     ;
   \end{rail}
 
   \begin{descr}
 
-  \item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text{\isachardoublequote}}] turns the
-  given ML expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type
-  \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> term| into an
-  ML function of type
-  \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> thm|, which is
-  bound to the global identifier \verb|name|.
+  \item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text{\isachardoublequote}}] turns the given ML
+  expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type \verb|'a -> cterm| into an
+  ML function of type \verb|'a -> thm|, which is bound to the
+  global identifier \verb|name|.
 
   \end{descr}%
 \end{isamarkuptext}%