# HG changeset patch
# User wenzelm
# Date 1126642766 -7200
# Node ID 92504e2f6c07d13477bb36587206a3a1a38d8cd5
# Parent  ca0e5105c4b12a20e10a16b8c9aace6fbf0dee84
added generic_setup, add_oracle (from isar_thy.ML);

diff -r ca0e5105c4b1 -r 92504e2f6c07 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Sep 13 22:19:25 2005 +0200
+++ b/src/Pure/pure_thy.ML	Tue Sep 13 22:19:26 2005 +0200
@@ -72,6 +72,8 @@
     theory -> theory * thm list list
   val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list ->
     theory -> theory * thm list list
+  val generic_setup: string -> theory -> theory
+  val add_oracle: bstring * string * string -> theory -> theory
 end;
 
 structure PureThy: PURE_THY =
@@ -445,6 +447,33 @@
 
 
 
+(*** ML setup ***)
+
+(* generic_setup *)
+
+val generic_setup =
+  Context.use_let "val setup: (theory -> theory) list" "Library.apply setup";
+
+
+(* add_oracle *)
+
+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;
+
+
+
 (*** the ProtoPure theory ***)
 
 val aT = TFree ("'a", []);