# HG changeset patch
# User haftmann
# Date 1273497673 -7200
# Node ID 929b23461a1470f07b5f5ebf18eb158dbf181d2c
# Parent  f4ad04780669984c9b62b3e1eca60cace880e828
simplified oracle

diff -r f4ad04780669 -r 929b23461a14 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 15:00:53 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 15:21:13 2010 +0200
@@ -11,7 +11,6 @@
   val del: term list -> attribute
   val add: term list -> attribute 
   val conv: Proof.context -> conv
-  val oracle: cterm -> thm
   val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
   val method: (Proof.context -> Method.method) context_parser
   exception COOPER of string * exn
@@ -676,18 +675,17 @@
  | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n))
  | _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!";
 
-fun raw_oracle ct =
+fun invoke t =
   let
-    val thy = Thm.theory_of_cterm ct;
-    val t = Thm.term_of ct;
     val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
   in
-    Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
-      HOLogic.mk_Trueprop (term_of_qf ps vs (Cooper_Procedure.pa (qf_of_term ps vs t)))))
+    Logic.mk_equals (HOLogic.mk_Trueprop t,
+      HOLogic.mk_Trueprop (term_of_qf ps vs (Cooper_Procedure.pa (qf_of_term ps vs t))))
   end;
 
 val (_, oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "cooper", raw_oracle)));
+  (Thm.add_oracle (Binding.name "cooper",
+    (fn (ctxt, t) => Thm.cterm_of (ProofContext.theory_of ctxt) (invoke t)))));
 
 val comp_ss = HOL_ss addsimps @{thms semiring_norm};
 
@@ -824,11 +822,10 @@
 end;
 
 fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
-   let 
+   let
     val cpth = 
        if !quick_and_dirty 
-       then oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
-             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
+       then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
        else Conv.arg_conv (conv ctxt) p
     val p' = Thm.rhs_of cpth
     val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))