src/HOL/Tools/Qelim/cooper.ML
changeset 36805 929b23461a14
parent 36804 f4ad04780669
child 36806 fc27b0465a4c
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 15:00:53 2010 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 15:21:13 2010 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4    val del: term list -> attribute
     1.5    val add: term list -> attribute 
     1.6    val conv: Proof.context -> conv
     1.7 -  val oracle: cterm -> thm
     1.8    val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
     1.9    val method: (Proof.context -> Method.method) context_parser
    1.10    exception COOPER of string * exn
    1.11 @@ -676,18 +675,17 @@
    1.12   | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n))
    1.13   | _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!";
    1.14  
    1.15 -fun raw_oracle ct =
    1.16 +fun invoke t =
    1.17    let
    1.18 -    val thy = Thm.theory_of_cterm ct;
    1.19 -    val t = Thm.term_of ct;
    1.20      val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
    1.21    in
    1.22 -    Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
    1.23 -      HOLogic.mk_Trueprop (term_of_qf ps vs (Cooper_Procedure.pa (qf_of_term ps vs t)))))
    1.24 +    Logic.mk_equals (HOLogic.mk_Trueprop t,
    1.25 +      HOLogic.mk_Trueprop (term_of_qf ps vs (Cooper_Procedure.pa (qf_of_term ps vs t))))
    1.26    end;
    1.27  
    1.28  val (_, oracle) = Context.>>> (Context.map_theory_result
    1.29 -  (Thm.add_oracle (Binding.name "cooper", raw_oracle)));
    1.30 +  (Thm.add_oracle (Binding.name "cooper",
    1.31 +    (fn (ctxt, t) => Thm.cterm_of (ProofContext.theory_of ctxt) (invoke t)))));
    1.32  
    1.33  val comp_ss = HOL_ss addsimps @{thms semiring_norm};
    1.34  
    1.35 @@ -824,11 +822,10 @@
    1.36  end;
    1.37  
    1.38  fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
    1.39 -   let 
    1.40 +   let
    1.41      val cpth = 
    1.42         if !quick_and_dirty 
    1.43 -       then oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
    1.44 -             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
    1.45 +       then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
    1.46         else Conv.arg_conv (conv ctxt) p
    1.47      val p' = Thm.rhs_of cpth
    1.48      val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))