# HG changeset patch
# User wenzelm
# Date 1169240899 -3600
# Node ID f9eb6328bdbdadf4576dfd5ddd72772b1416231c
# Parent  9188aed2c3ca0b541af6d4d0883046e7790baf0f
moved thm/thms to ml_context.ML;
moved generic_setup, add_oracle to isar_cmd.ML;

diff -r 9188aed2c3ca -r f9eb6328bdbd src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Jan 19 22:08:18 2007 +0100
+++ b/src/Pure/pure_thy.ML	Fri Jan 19 22:08:19 2007 +0100
@@ -15,8 +15,6 @@
   val get_thm: theory -> thmref -> thm
   val get_thms: theory -> thmref -> thm list
   val get_thmss: theory -> thmref list -> thm list
-  val thm: xstring -> thm
-  val thms: xstring -> thm list
   structure ProtoPure:
     sig
       val thy: theory
@@ -98,8 +96,6 @@
     theory -> thm list list * theory
   val add_defss_i: bool -> ((bstring * term list) * attribute list) list ->
     theory -> thm list list * theory
-  val generic_setup: string option -> theory -> theory
-  val add_oracle: bstring * string * string -> theory -> theory
 end;
 
 structure PureThy: PURE_THY =
@@ -280,9 +276,6 @@
 fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs;
 fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);
 
-fun thm name = get_thm (the_context ()) (Name name);
-fun thms name = get_thms (the_context ()) (Name name);
-
 
 (* thms_containing etc. *)
 
@@ -501,36 +494,6 @@
 
 
 
-(*** ML setup ***)
-
-(* generic_setup *)
-
-fun generic_setup NONE = (fn thy => thy |> Context.setup ())
-  | generic_setup (SOME txt) =
-      Context.use_let "val setup: theory -> theory" "Context.map_theory setup" txt
-      |> Context.theory_map;
-
-
-(* 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_update txt false end
-  |> Context.theory_map;
-
-
-
 (*** the ProtoPure theory ***)
 
 val aT = TFree ("'a", []);