# HG changeset patch
# User wenzelm
# Date 1221759584 -7200
# Node ID 4cc2b6046258168627a5a22efefa2bec4ce80bc9
# Parent  efd53393412b8a2e9ed4adb63356f24f3e5171c1
simplified oracle interface;

diff -r efd53393412b -r 4cc2b6046258 NEWS
--- a/NEWS	Thu Sep 18 14:06:58 2008 +0200
+++ b/NEWS	Thu Sep 18 19:39:44 2008 +0200
@@ -22,6 +22,13 @@
 
 *** Pure ***
 
+* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
+to 'a -> thm, at the cost of internal tagging of results with an
+authentic oracle name.  The Isar command 'oracle' is now polymorphic,
+no argument type is specified.  INCOMPATIBILITY, need to simplify
+existing oracle code accordingly.  Note that extra performance may be
+gained by producing the cterm carefully, not via Thm.cterm_of.
+
 * Changed defaults for unify configuration options:
 
   unify_trace_bound = 50 (formerly 25)
diff -r efd53393412b -r 4cc2b6046258 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -595,12 +595,12 @@
   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
   @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
-  @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
+  @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
+  -> (string * ('a -> thm)) * theory"} \\
   \end{mldecls}
   \begin{mldecls}
   @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
   @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
-  @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
   @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
   \end{mldecls}
 
@@ -651,16 +651,13 @@
   \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
 
-  \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a
-  named oracle function, cf.\ @{text "axiom"} in
-  \figref{fig:prim-rules}.
+  \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
+  oracle rule, essentially generating arbitrary axioms on the fly,
+  cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
 
   \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
   arbitrary propositions as axioms.
 
-  \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle
-  function for generating arbitrary axioms on the fly.
-
   \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
   \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
   for constant @{text "c\<^isub>\<tau>"}, relative to existing
diff -r efd53393412b -r 4cc2b6046258 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -1136,9 +1136,8 @@
     @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
   \end{matharray}
 
-  The oracle interface promotes a given ML function @{ML_text
-  "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some
-  type @{ML_text T} given by the user.  This acts like an infinitary
+  The oracle interface promotes a given ML function @{ML_text "'a -> cterm"}
+  to @{ML_text "'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
@@ -1146,18 +1145,16 @@
   that are not fully checked by Isabelle inferences.
 
   \begin{rail}
-    'oracle' name '(' type ')' '=' text
+    'oracle' name '=' text
     ;
   \end{rail}
 
   \begin{descr}
 
-  \item [@{command "oracle"}~@{text "name (type) = text"}] turns the
-  given ML expression @{text "text"} of type
-  @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an
-  ML function of type
-  @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is
-  bound to the global identifier @{ML_text name}.
+  \item [@{command "oracle"}~@{text "name = text"}] turns the given ML
+  expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
+  ML function of type @{ML_text "'a -> thm"}, which is bound to the
+  global identifier @{ML_text name}.
 
   \end{descr}
 *}
diff -r efd53393412b -r 4cc2b6046258 src/FOL/ex/IffOracle.thy
--- a/src/FOL/ex/IffOracle.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/FOL/ex/IffOracle.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -18,14 +18,14 @@
   and positive.
 *}
 
-oracle iff_oracle (int) = {*
+oracle iff_oracle = {*
   let
     fun mk_iff 1 = Var (("P", 0), @{typ o})
       | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);
   in
-    fn thy => fn n =>
+    fn (thy, n) =>
       if n > 0 andalso n mod 2 = 0
-      then FOLogic.mk_Trueprop (mk_iff n)
+      then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n))
       else raise Fail ("iff_oracle: " ^ string_of_int n)
   end
 *}
@@ -33,19 +33,19 @@
 
 subsection {* Oracle as low-level rule *}
 
-ML {* iff_oracle @{theory} 2 *}
-ML {* iff_oracle @{theory} 10 *}
-ML {* #der (Thm.rep_thm (iff_oracle @{theory} 10)) *}
+ML {* iff_oracle (@{theory}, 2) *}
+ML {* iff_oracle (@{theory}, 10) *}
+ML {* #der (Thm.rep_thm (iff_oracle (@{theory}, 10))) *}
 
 text {* These oracle calls had better fail. *}
 
 ML {*
-  (iff_oracle @{theory} 5; error "?")
+  (iff_oracle (@{theory}, 5); error "?")
     handle Fail _ => warning "Oracle failed, as expected"
 *}
 
 ML {*
-  (iff_oracle @{theory} 1; error "?")
+  (iff_oracle (@{theory}, 1); error "?")
     handle Fail _ => warning "Oracle failed, as expected"
 *}
 
@@ -55,7 +55,7 @@
 method_setup iff = {*
   Method.simple_args OuterParse.nat (fn n => fn ctxt =>
     Method.SIMPLE_METHOD
-      (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))
+      (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
         handle Fail _ => no_tac))
 *} "iff oracle"
 
diff -r efd53393412b -r 4cc2b6046258 src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ATP_Linkup.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -101,9 +101,9 @@
 
 use "Tools/res_atp_provers.ML"
 
-oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
-oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
-oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
+oracle vampire_oracle = {* ResAtpProvers.vampire_o *}
+oracle eprover_oracle = {* ResAtpProvers.eprover_o *}
+oracle spass_oracle = {* ResAtpProvers.spass_o *}
 
 use "Tools/res_atp_methods.ML"
 setup ResAtpMethods.setup      --{*Oracle ATP methods: still useful?*}
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Code_Setup.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -129,17 +129,22 @@
 end;
 *}
 
-oracle eval_oracle ("term") = {* fn thy => fn t => 
-  if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
-    (HOLogic.dest_Trueprop t) [] 
-  then t
-  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
+oracle eval_oracle = {* fn ct =>
+  let
+    val thy = Thm.theory_of_cterm ct;
+    val t = Thm.term_of ct;
+  in
+    if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
+      (HOLogic.dest_Trueprop t) [] 
+    then ct
+    else @{cprop True} (*dummy*)
+  end
 *}
 
 method_setup eval = {*
 let
   fun eval_tac thy = 
-    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
+    CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
 in 
   Method.ctxt_args (fn ctxt => 
     Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Complex/ex/MIR.thy
--- a/src/HOL/Complex/ex/MIR.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Complex/ex/MIR.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -5791,7 +5791,7 @@
 (*export_code mircfrqe mirlfrqe
   in SML module_name Mir file "raw_mir.ML"*)
 
-oracle mirfr_oracle ("bool * term") = {*
+oracle mirfr_oracle = {* fn (proofs, ct) =>
 let
 
 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
@@ -5891,13 +5891,15 @@
   | term_of_fm vs (@{code Iff} (t1, t2)) =
       @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ term_of_fm vs t1 $ term_of_fm vs t2;
 
-in fn thy => fn (proofs, t) =>
+in
   let 
+    val thy = Thm.theory_of_cterm ct;
+    val t = Thm.term_of ct;
     val fs = term_frees t;
     val vs = fs ~~ (0 upto (length fs - 1));
     val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
     val t' = (term_of_fm vs o qe o fm_of_term vs) t;
-  in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+  in (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
 end;
 *}
 
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -1997,7 +1997,7 @@
 
 ML {* @{code ferrack_test} () *}
 
-oracle linr_oracle ("term") = {*
+oracle linr_oracle = {*
 let
 
 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
@@ -2066,11 +2066,14 @@
       term_of_fm vs t1 $ term_of_fm vs t2
   | term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent.";
 
-in fn thy => fn t =>
+in fn ct =>
   let 
+    val thy = Thm.theory_of_cterm ct;
+    val t = Thm.term_of ct;
     val fs = term_frees t;
     val vs = fs ~~ (0 upto (length fs - 1));
-  in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t)))) end
+    val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
+  in Thm.cterm_of thy res end
 end;
 *}
 
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Complex/ex/linrtac.ML
--- a/src/HOL/Complex/ex/linrtac.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Complex/ex/linrtac.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -86,7 +86,7 @@
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
-    let val pth = linr_oracle thy (Pattern.eta_long [] t1)
+    let val pth = linr_oracle (cterm_of thy (Pattern.eta_long [] t1))
     in 
           (trace_msg ("calling procedure with term:\n" ^
              Syntax.string_of_term ctxt t1);
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Complex/ex/mirtac.ML
--- a/src/HOL/Complex/ex/mirtac.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Complex/ex/mirtac.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -87,9 +87,9 @@
 
 fun mir_tac ctxt q i = 
     (ObjectLogic.atomize_prems_tac i)
-	THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
-	THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
-	THEN (fn st =>
+        THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
+        THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
+        THEN (fn st =>
   let
     val g = List.nth (prems_of st, i - 1)
     val thy = ProofContext.theory_of ctxt
@@ -97,13 +97,13 @@
     val (t,np,nh) = prepare_for_mir thy q g
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset = HOL_basic_ss 
-			addsimps [refl,nat_mod_add_eq, 
-				  @{thm "mod_self"}, @{thm "zmod_self"},
-				  @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
-				  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
-				  @{thm "Suc_plus1"}]
-			addsimps @{thms add_ac}
-			addsimprocs [cancel_div_mod_proc]
+                        addsimps [refl,nat_mod_add_eq, 
+                                  @{thm "mod_self"}, @{thm "zmod_self"},
+                                  @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
+                                  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
+                                  @{thm "Suc_plus1"}]
+                        addsimps @{thms add_ac}
+                        addsimprocs [cancel_div_mod_proc]
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
       addsimps comp_ths
@@ -131,11 +131,11 @@
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
-    let val pth = 
+    let val pth =
           (* If quick_and_dirty then run without proof generation as oracle*)
-             if !quick_and_dirty 
-             then mirfr_oracle thy (false, Pattern.eta_long [] t1)
-	     else mirfr_oracle thy (true, Pattern.eta_long [] t1)
+             if !quick_and_dirty
+             then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
+             else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
     in 
           (trace_msg ("calling procedure with term:\n" ^
              Syntax.string_of_term ctxt t1);
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -55,8 +55,10 @@
 end;
 *}
 
-oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) => 
+oracle eval_witness_oracle = {* fn (cgoal, ws) =>
 let
+  val thy = Thm.theory_of_cterm cgoal;
+  val goal = Thm.term_of cgoal;
   fun check_type T = 
     if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
     then T
@@ -69,8 +71,8 @@
   val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
 in
   if Code_ML.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
-  then goal
-  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
+  then Thm.cterm_of thy goal
+  else @{cprop True} (*dummy*)
 end
 *}
 
@@ -78,12 +80,11 @@
 method_setup eval_witness = {*
 let
 
-fun eval_tac ws thy = 
-  SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i)
+fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)
 
-in 
-  Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt => 
-    Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt)))
+in
+  Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
+    Method.SIMPLE_METHOD' (eval_tac ws))
 end
 *} "Evaluation with ML witnesses"
 
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Modelcheck/EindhovenSyn.thy
--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -30,7 +30,7 @@
   val trace_eindhoven = ref false;
 *}
 
-oracle mc_eindhoven_oracle ("term") =
+oracle mc_eindhoven_oracle =
 {*
 let
   val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
@@ -43,15 +43,17 @@
         else eindhoven_home ^ "/pmu";
     in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
 in
-  fn thy => fn goal =>
+  fn cgoal =>
     let
+      val thy = Thm.theory_of_cterm cgoal;
+      val goal = Thm.term_of cgoal;
       val s = eindhoven_term thy goal;
       val debug = tracing ("MC debugger: " ^ s);
       val result = call_mc s;
     in
       if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else ();
       (case result of
-        "TRUE\n"  => goal |
+        "TRUE\n"  => cgoal |
         "FALSE\n" => error "MC oracle yields FALSE" |
       _ => error ("MC syntax error: " ^ result))
     end
@@ -62,7 +64,7 @@
 fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
   let
     val thy = Thm.theory_of_thm state;
-    val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
+    val assertion = mc_eindhoven_oracle (Thm.cterm_of thy (Logic.strip_imp_concl goal));
   in cut_facts_tac [assertion] i THEN atac i end) i state;
 
 val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -68,8 +68,7 @@
   will be replaced by the expression between the two asterisks
   following "case" and the asterisk after esac will be deleted *)
 
-oracle mc_mucke_oracle ("term") =
-  mk_mc_mucke_oracle
+oracle mc_mucke_oracle = mk_mc_mucke_oracle
 
 ML {*
 (* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
@@ -154,12 +153,9 @@
 end;
 
 
-fun call_mucke_tac i state =
-let val thy = Thm.theory_of_thm state;
-    val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
-in 
-(cut_facts_tac [OraAss] i) state
-end;
+val call_mucke_tac = CSUBGOAL (fn (cgoal, i) =>
+let val OraAss = mc_mucke_oracle cgoal
+in cut_facts_tac [OraAss] i end);
 
 
 (* transforming fun-defs into lambda-defs *)
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -1012,8 +1012,12 @@
 
 (**********************************************************)
 
-fun mk_mc_mucke_oracle sign subgoal = 
-  let 	val Freesubgoal = freeze_thaw subgoal;
+fun mk_mc_mucke_oracle csubgoal =
+  let
+  val sign = Thm.theory_of_cterm csubgoal;
+  val subgoal = Thm.term_of csubgoal;
+
+	val Freesubgoal = freeze_thaw subgoal;
 
 	val prems = Logic.strip_imp_prems Freesubgoal; 
 	val concl = Logic.strip_imp_concl Freesubgoal; 
@@ -1047,6 +1051,6 @@
 	(writeln ("\nmodelchecker input:\n" ^ MCstr ^ "\n/**** end ****/"))
           else ();
 (case (extract_result concl_str result) of 
-	true  =>  (Logic.strip_imp_concl subgoal) | 
+	true  =>  cterm_of sign (Logic.strip_imp_concl subgoal) | 
 	false => (error ("Mucke couldn't solve subgoal: \n" ^result)))) 
   end;
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Presburger.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -440,7 +440,7 @@
 by simp_all
 
 use "Tools/Qelim/cooper.ML"
-oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
+oracle linzqe_oracle = Coopereif.cooper_oracle
 
 use "Tools/Qelim/presburger.ML"
 
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -633,12 +633,14 @@
  | NClosed n => term_of_qf ps vs (Nota (Closed n))
  | _ => cooper "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
 
-fun cooper_oracle thy t = 
+fun cooper_oracle ct =
   let
+    val thy = Thm.theory_of_cterm ct;
+    val t = Thm.term_of ct;
     val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
   in
-    Logic.mk_equals (HOLogic.mk_Trueprop t,
-      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
+    Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
+      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))))
   end;
 
 end;
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -152,8 +152,8 @@
    let 
     val cpth = 
        if !quick_and_dirty 
-       then linzqe_oracle (ProofContext.theory_of ctxt) 
-             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
+       then linzqe_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
+             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
        else arg_conv (Cooper.cooper_conv ctxt) p
     val p' = Thm.rhs_of cpth
     val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Tools/res_atp_methods.ML
--- a/src/HOL/Tools/res_atp_methods.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Tools/res_atp_methods.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -27,7 +27,7 @@
     Meson.skolemize_tac,
     METAHYPS (fn negs =>
       HEADGOAL (Tactic.rtac
-        (res_atp_oracle (ProofContext.theory_of ctxt)
+        (res_atp_oracle
           (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms i, timeLimit))))] i st) handle Fail _ => Seq.empty;
 
 
diff -r efd53393412b -r 4cc2b6046258 src/HOL/Tools/res_atp_provers.ML
--- a/src/HOL/Tools/res_atp_provers.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Tools/res_atp_provers.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -40,19 +40,19 @@
   in seek_line "SPASS beiseite: Proof found.\n" instr
   end;
 
-fun vampire_o _ (file,time) =
+fun vampire_o (file,time) =
   if call_vampire (file,time)
-  then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
+  then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
   else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
 
-fun eprover_o _ (file,time) =
+fun eprover_o (file,time) =
   if call_eprover (file,time)
-  then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
+  then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
   else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
 
-fun spass_o _ (file,time) =
+fun spass_o (file,time) =
   if call_spass (file,time)
-  then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
+  then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
   else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
 
 end;
diff -r efd53393412b -r 4cc2b6046258 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -1920,7 +1920,7 @@
 export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"
 *)
 
-oracle linzqe_oracle ("term") = {*
+oracle linzqe_oracle = {*
 let
 
 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
@@ -2035,14 +2035,16 @@
     | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
   end;
 
-in fn thy => fn t =>
-  let 
+in fn ct =>
+  let
+    val thy = Thm.theory_of_cterm ct;
+    val t = Thm.term_of ct;
     val fs = term_frees t;
     val bs = term_bools [] t;
     val vs = fs ~~ (0 upto (length fs - 1))
     val ps = bs ~~ (0 upto (length bs - 1))
     val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
-  in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+  in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
 end;
 *}
 
diff -r efd53393412b -r 4cc2b6046258 src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -19,8 +19,7 @@
 
 hide const iff_keep iff_unfold
 
-oracle
-  svc_oracle ("term") = Svc.oracle
+oracle svc_oracle = Svc.oracle
 
 ML {*
 (*
@@ -110,12 +109,13 @@
   abstracted.  Use via compose_tac, which performs no lifting but will
   instantiate variables.*)
 
-fun svc_tac i st =
+val svc_tac = CSUBGOAL (fn (ct, i) =>
   let
-    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
-    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
-   in compose_tac (false, th, 0) i st end
-   handle TERM _ => no_tac st;
+    val thy = Thm.theory_of_cterm ct;
+    val (abs_goal, _) = svc_abstract (Thm.term_of ct);
+    val th = svc_oracle (Thm.cterm_of thy abs_goal);
+   in compose_tac (false, th, 0) i end
+   handle TERM _ => no_tac);
 *}
 
 end
diff -r efd53393412b -r 4cc2b6046258 src/HOL/ex/coopertac.ML
--- a/src/HOL/ex/coopertac.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ex/coopertac.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -104,7 +104,7 @@
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
-    let val pth = linzqe_oracle thy (Pattern.eta_long [] t1)
+    let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
     in 
           ((pth RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
diff -r efd53393412b -r 4cc2b6046258 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -237,10 +237,14 @@
   end;
 
 
- (*The oracle proves the given formula t, if possible*)
- fun oracle thy t =
-  (if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
-   else ();
-   if valid (expr_of false t) then t else fail t);
+ (*The oracle proves the given formula, if possible*)
+  fun oracle ct =
+    let
+      val thy = Thm.theory_of_cterm ct;
+      val t = Thm.term_of ct;
+      val _ =
+        if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
+       else ();
+    in if valid (expr_of false t) then ct else fail t end;
 
 end;
diff -r efd53393412b -r 4cc2b6046258 src/HOLCF/IOA/Modelcheck/MuIOA.thy
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -178,8 +178,12 @@
 
 in
 
-fun mk_sim_oracle sign (subgoal, thl) = (
+fun mk_sim_oracle (csubgoal, thl) =
   let
+    val sign = Thm.theory_of_cterm csubgoal;
+    val subgoal = Thm.term_of csubgoal;
+  in
+ (let
     val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
     val concl = Logic.strip_imp_concl subgoal;
     val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
@@ -287,11 +291,12 @@
 by (atac 1);
 result();
 OldGoals.pop_proof();
-Logic.strip_imp_concl subgoal
+Thm.cterm_of sign (Logic.strip_imp_concl subgoal)
 )
 end)
 handle malformed =>
-error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal));
+error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal))
+end;
 
 end
 
diff -r efd53393412b -r 4cc2b6046258 src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -5,16 +5,13 @@
 imports MuIOA
 begin
 
-oracle sim_oracle ("term * thm list") =
-  mk_sim_oracle
+oracle sim_oracle = mk_sim_oracle
 
 ML {*
 (* call_sim_tac invokes oracle "Sim" *)
-fun call_sim_tac thm_list i state = 
-let val thy = Thm.theory_of_thm state;
-        val (subgoal::_) = Library.drop(i-1,prems_of state);
-        val OraAss = sim_oracle thy (subgoal,thm_list);
-in cut_facts_tac [OraAss] i state end;
+fun call_sim_tac thm_list = CSUBGOAL (fn (csubgoal, i) =>
+let val OraAss = sim_oracle (csubgoal,thm_list);
+in cut_facts_tac [OraAss] i end);
 
 
 val ioa_implements_def = thm "ioa_implements_def";
diff -r efd53393412b -r 4cc2b6046258 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -13,8 +13,7 @@
   val print_translation: bool * (string * Position.T) -> theory -> theory
   val typed_print_translation: bool * (string * Position.T) -> theory -> theory
   val print_ast_translation: bool * (string * Position.T) -> theory -> theory
-  val oracle: bstring -> SymbolPos.text * Position.T -> SymbolPos.text * Position.T ->
-    theory -> theory
+  val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory
   val add_axioms: ((Name.binding * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((Name.binding * string) * Attrib.src list) list -> theory -> theory
   val declaration: string * Position.T -> local_theory -> local_theory
@@ -152,22 +151,15 @@
 
 (* oracles *)
 
-fun oracle name typ_pos (oracle_txt, pos) =
+fun oracle name (oracle_txt, pos) =
   let
-    val typ = SymbolPos.content (SymbolPos.explode typ_pos);
     val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos));
     val txt =
-      "local\
-      \  type T = " ^ typ ^ ";\
-      \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
+      "local\n\
       \  val name = " ^ quote name ^ ";\n\
-      \  exception Arg of T;\n\
-      \  val _ = Context.>> (Context.map_theory\n\
-      \    (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
-      \  val thy = ML_Context.the_global_context ();\n\
-      \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
+      \  val oracle = " ^ oracle ^ ";\n\
       \in\n\
-      \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
+      \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (name, oracle))));\n\
       \end;\n";
   in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
 
diff -r efd53393412b -r 4cc2b6046258 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -371,8 +371,7 @@
 
 val _ =
   OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
-    (P.name -- (P.$$$ "(" |-- P.ML_source --| P.$$$ ")" --| P.$$$ "=")
-      -- P.ML_source >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
+    (P.name -- (P.$$$ "=" |-- P.ML_source) >> (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
 
 
 (* local theories *)
diff -r efd53393412b -r 4cc2b6046258 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -20,20 +20,15 @@
 
 (* oracle setup *)
 
-exception SkipProof of term;
-
-fun skip_proof (_, SkipProof prop) =
-  if ! quick_and_dirty then prop
-  else error "Proof may be skipped in quick_and_dirty mode only!";
-
-val _ = Context.>> (Context.map_theory
-  (Theory.add_oracle ("skip_proof", skip_proof)));
+val (_, skip_proof) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle ("skip_proof", fn (thy, prop) =>
+    if ! quick_and_dirty then Thm.cterm_of thy prop
+    else error "Proof may be skipped in quick_and_dirty mode only!")));
 
 
 (* basic cheating *)
 
-fun make_thm thy prop =
-  Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
+fun make_thm thy prop = skip_proof (thy, prop);
 
 fun cheat_tac thy st =
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
diff -r efd53393412b -r 4cc2b6046258 src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/display.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -178,7 +178,6 @@
       Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
 
     val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
-    val oracles = (Theory.oracle_space thy, Theory.oracle_table thy);
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
     val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
@@ -202,7 +201,6 @@
     val cnstrs = NameSpace.extern_table constraints;
 
     val axms = NameSpace.extern_table axioms;
-    val oras = NameSpace.extern_table oracles;
 
     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
@@ -223,7 +221,7 @@
       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
       Pretty.big_list "axioms:" (map pretty_axm axms),
-      Pretty.strs ("oracles:" :: (map #1 oras)),
+      Pretty.strs ("oracles:" :: Thm.extern_oracles thy),
       Pretty.big_list "definitions:"
         [pretty_finals reds0,
          Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
diff -r efd53393412b -r 4cc2b6046258 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/theory.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Lawrence C Paulson and Markus Wenzel
 
-Logical theory content: axioms, definitions, oracles.
+Logical theory content: axioms, definitions, and begin/end wrappers.
 *)
 
 signature THEORY =
@@ -22,8 +22,6 @@
   val requires: theory -> string -> string -> unit
   val axiom_space: theory -> NameSpace.T
   val axiom_table: theory -> term Symtab.table
-  val oracle_space: theory -> NameSpace.T
-  val oracle_table: theory -> ((theory * Object.T -> term) * stamp) Symtab.table
   val axioms_of: theory -> (string * term) list
   val all_axioms_of: theory -> (string * term) list
   val defs_of: theory -> Defs.T
@@ -39,7 +37,6 @@
   val add_finals: bool -> string list -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
   val specify_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
-  val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
 end
 
 structure Theory: THEORY =
@@ -86,55 +83,41 @@
 datatype thy = Thy of
  {axioms: term NameSpace.table,
   defs: Defs.T,
-  oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
   wrappers: wrapper list * wrapper list};
 
-fun make_thy (axioms, defs, oracles, wrappers) =
-  Thy {axioms = axioms, defs = defs, oracles = oracles, wrappers = wrappers};
+fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
 
 fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
-fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
 
 structure ThyData = TheoryDataFun
 (
   type T = thy;
-  val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, ([], []));
+  val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
   val copy = I;
 
-  fun extend (Thy {axioms, defs, oracles, wrappers}) =
-    make_thy (NameSpace.empty_table, defs, oracles, wrappers);
+  fun extend (Thy {axioms, defs, wrappers}) = make_thy (NameSpace.empty_table, defs, wrappers);
 
   fun merge pp (thy1, thy2) =
     let
-      val Thy {axioms = _, defs = defs1, oracles = oracles1, wrappers = (bgs1, ens1)} = thy1;
-      val Thy {axioms = _, defs = defs2, oracles = oracles2, wrappers = (bgs2, ens2)} = thy2;
+      val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
+      val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
       val axioms' = NameSpace.empty_table;
       val defs' = Defs.merge pp (defs1, defs2);
-      val oracles' = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
-        handle Symtab.DUP dup => err_dup_ora dup;
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
-    in make_thy (axioms', defs', oracles', (bgs', ens')) end;
+    in make_thy (axioms', defs', (bgs', ens')) end;
 );
 
 fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
 
-fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, wrappers}) =>
-  make_thy (f (axioms, defs, oracles, wrappers)));
+fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
+  make_thy (f (axioms, defs, wrappers)));
 
 
-fun map_axioms f = map_thy
-  (fn (axioms, defs, oracles, wrappers) => (f axioms, defs, oracles, wrappers));
-
-fun map_defs f = map_thy
-  (fn (axioms, defs, oracles, wrappers) => (axioms, f defs, oracles, wrappers));
-
-fun map_oracles f = map_thy
-  (fn (axioms, defs, oracles, wrappers) => (axioms, defs, f oracles, wrappers));
-
-fun map_wrappers f = map_thy
-  (fn (axioms, defs, oracles, wrappers) => (axioms, defs, oracles, f wrappers));
+fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
+fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));
+fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers));
 
 
 (* basic operations *)
@@ -142,9 +125,6 @@
 val axiom_space = #1 o #axioms o rep_theory;
 val axiom_table = #2 o #axioms o rep_theory;
 
-val oracle_space = #1 o #oracles o rep_theory;
-val oracle_table = #2 o #oracles o rep_theory;
-
 val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
 fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
 
@@ -323,13 +303,4 @@
 
 end;
 
-
-
-(** add oracle **)
-
-fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
-  NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
-    handle Symtab.DUP dup => err_dup_ora dup);
-
 end;
-
diff -r efd53393412b -r 4cc2b6046258 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/thm.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -112,8 +112,8 @@
   val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
   val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
-  val invoke_oracle: theory -> xstring -> theory * Object.T -> thm
-  val invoke_oracle_i: theory -> string -> theory * Object.T -> thm
+  val extern_oracles: theory -> xstring list
+  val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
 
 signature THM =
@@ -1557,36 +1557,53 @@
 
 (*** Oracles ***)
 
-fun invoke_oracle_i thy1 name =
-  let
-    val oracle =
-      (case Symtab.lookup (Theory.oracle_table thy1) name of
-        NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
-      | SOME (f, _) => f);
-    val thy_ref1 = Theory.check_thy thy1;
-  in
-    fn (thy2, data) =>
-      let
-        val thy' = Theory.merge (Theory.deref thy_ref1, thy2);
-        val (prop, T, maxidx) = Sign.certify_term thy' (oracle (thy', data));
-        val shyps' = Sorts.insert_term prop [];
-        val der = Deriv.oracle name prop;
-      in
-        if T <> propT then
-          raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
-        else
-          Thm {thy_ref = Theory.check_thy thy', der = der, tags = [],
-            maxidx = maxidx, shyps = shyps', hyps = [], tpairs = [], prop = prop}
-      end
+(* oracle rule *)
+
+fun invoke_oracle thy_ref1 name oracle arg =
+  let val {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = rep_cterm (oracle arg) in
+    if T <> propT then
+      raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
+    else
+      Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
+        der = Deriv.oracle name prop,
+        tags = [],
+        maxidx = maxidx,
+        shyps = sorts,
+        hyps = [],
+        tpairs = [],
+        prop = prop}
   end;
 
-fun invoke_oracle thy =
-  invoke_oracle_i thy o NameSpace.intern (Theory.oracle_space thy);
-
-
 end;
 end;
 end;
+
+
+(* authentic derivation names *)
+
+fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
+
+structure Oracles = TheoryDataFun
+(
+  type T = stamp NameSpace.table;
+  val empty = NameSpace.empty_table;
+  val copy = I;
+  val extend = I;
+  fun merge _ oracles = NameSpace.merge_tables (op =) oracles
+    handle Symtab.DUP dup => err_dup_ora dup;
+);
+
+val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
+
+fun add_oracle (bname, oracle) thy =
+  let
+    val naming = Sign.naming_of thy;
+    val name = NameSpace.full naming bname;
+    val thy' = thy |> Oracles.map (fn (space, tab) =>
+      (NameSpace.declare naming name space,
+        Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
+  in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
+
 end;
 
 structure BasicThm: BASIC_THM = Thm;
diff -r efd53393412b -r 4cc2b6046258 src/Tools/Compute_Oracle/Compute_Oracle.thy
--- a/src/Tools/Compute_Oracle/Compute_Oracle.thy	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy	Thu Sep 18 19:39:44 2008 +0200
@@ -9,6 +9,4 @@
 uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
 begin
 
-setup {* Compute.setup_compute *}
-
 end
\ No newline at end of file
diff -r efd53393412b -r 4cc2b6046258 src/Tools/Compute_Oracle/compute.ML
--- a/src/Tools/Compute_Oracle/compute.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -35,8 +35,6 @@
     (* ! *) val evaluate_prem : computer -> int -> theorem -> theorem
     (* ! *) val modus_ponens : computer -> int -> thm -> theorem -> theorem
 
-    val setup_compute : theory -> theory
-
 end
 
 structure Compute :> COMPUTE = struct
@@ -362,8 +360,6 @@
 (* An oracle for exporting theorems; must only be accessible from inside this structure! *)
 (* ------------------------------------------------------------------------------------- *)
 
-exception ExportThm of term list * sort list * term
-
 fun merge_hyps hyps1 hyps2 = 
 let
     fun add hyps tab = fold (fn h => fn tab => Termtab.update (h, ()) tab) hyps tab
@@ -375,7 +371,8 @@
 
 fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
 
-fun export_oracle (thy, ExportThm (hyps, shyps, prop)) =
+val (_, export_oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle ("compute", fn (thy, hyps, shyps, prop) =>
     let
         val shyptab = add_shyps shyps Sorttab.empty
         fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
@@ -385,15 +382,12 @@
         val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
         val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
     in
-        fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop
-    end
-  | export_oracle _ = raise Match
-
-val setup_compute = (fn thy => Theory.add_oracle ("compute", export_oracle) thy)
+        Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
+    end)));
 
 fun export_thm thy hyps shyps prop =
     let
-        val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop))
+        val th = export_oracle (thy, hyps, shyps, prop)
         val hyps = map (fn h => assume (cterm_of thy h)) hyps
     in
         fold (fn h => fn p => implies_elim p h) hyps th 
diff -r efd53393412b -r 4cc2b6046258 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Tools/nbe.ML	Thu Sep 18 19:39:44 2008 +0200
@@ -403,15 +403,9 @@
 
 (* evaluation oracle *)
 
-exception Norm of term * Code_Thingol.program
-  * (Code_Thingol.typscheme * Code_Thingol.iterm) * string list;
-
-fun norm_oracle (thy, Norm (t, program, vs_ty_t, deps)) =
-  Logic.mk_equals (t, eval thy t program vs_ty_t deps);
-
-fun norm_invoke thy t program vs_ty_t deps =
-  Thm.invoke_oracle_i thy "HOL.norm" (thy, Norm (t, program, vs_ty_t, deps));
-  (*FIXME get rid of hardwired theory name*)
+val (_, norm_oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle ("norm", fn (thy, t, program, vs_ty_t, deps) =>
+    Thm.cterm_of thy (Logic.mk_equals (t, eval thy t program vs_ty_t deps)))));
 
 fun add_triv_classes thy =
   let
@@ -425,7 +419,7 @@
 fun norm_conv ct =
   let
     val thy = Thm.theory_of_cterm ct;
-    fun evaluator' t program vs_ty_t deps = norm_invoke thy t program vs_ty_t deps;
+    fun evaluator' t program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
     fun evaluator t = (add_triv_classes thy t, evaluator' t);
   in Code_Thingol.eval_conv thy evaluator ct end;
 
@@ -455,8 +449,8 @@
   let val ctxt = Toplevel.context_of state
   in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
 
-val setup = Theory.add_oracle ("norm", norm_oracle)
-  #> Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
+val setup =
+  Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
 
 local structure P = OuterParse and K = OuterKeyword in