# HG changeset patch
# User wenzelm
# Date 1121362113 -7200
# Node ID a6cdb1ade95591dc3b488d199abb7a0ea5481326
# Parent  1c8a5bb7c6880955322807c310b735c8d7e01eb4
type-safe 'oracle' command;

diff -r 1c8a5bb7c688 -r a6cdb1ade955 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 14 19:28:32 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 14 19:28:33 2005 +0200
@@ -292,8 +292,9 @@
 (* oracles *)
 
 val oracleP =
-  OuterSyntax.command "oracle" "install oracle" K.thy_decl
-    ((P.name --| P.$$$ "=") -- P.text >> (Toplevel.theory o IsarThy.add_oracle));
+  OuterSyntax.command "oracle" "declare oracle" K.thy_decl
+    (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
+      -- P.text >> (Toplevel.theory o IsarThy.add_oracle o P.triple1));
 
 
 (* locales *)
diff -r 1c8a5bb7c688 -r a6cdb1ade955 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Jul 14 19:28:32 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Jul 14 19:28:33 2005 +0200
@@ -153,7 +153,7 @@
   val token_translation: string -> theory -> theory
   val generic_setup: string -> theory -> theory
   val method_setup: bstring * string * string -> theory -> theory
-  val add_oracle: bstring * string -> theory -> theory
+  val add_oracle: bstring * string * string -> theory -> theory
   val add_locale: bool * bstring * Locale.expr * Locale.element list -> theory -> theory
   val register_globally:
     ((string * Attrib.src list) * Locale.expr) * string option list ->
@@ -615,11 +615,20 @@
 
 (* add_oracle *)
 
-fun add_oracle (name, txt) =
-  Context.use_let
-    "val oracle: bstring * (theory * Object.T -> term)"
-    "Theory.add_oracle oracle"
-    ("(" ^ Library.quote name ^ ", " ^ txt ^ ")");
+fun add_oracle (name, T, oracle) =
+  let val txt =
+    "local\n\
+    \  type T = " ^ T ^ ";\n\
+    \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
+    \  val name = " ^ quote name ^ ";\n\
+    \  exception Arg of T;\n\
+    \  val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
+    \  val thy = Context.the_context ();\n\
+    \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
+    \in\n\
+    \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
+    \end;\n";
+  in Context.use_mltext_theory txt false end;
 
 
 (* add_locale *)