src/HOL/Tools/Qelim/cooper.ML
changeset 38808 89ae86205739
parent 38795 848be46708dc
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 17:23:57 2010 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 17:59:40 2010 +0200
     1.3 @@ -679,9 +679,11 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -val (_, oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "cooper",
     1.8 -  (fn (ctxt, t) => (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
     1.9 -    (t, procedure t)))));
    1.10 +val (_, oracle) = Context.>>> (Context.map_theory_result
    1.11 +  (Thm.add_oracle (@{binding cooper},
    1.12 +    (fn (ctxt, t) =>
    1.13 +      (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
    1.14 +        (t, procedure t)))));
    1.15  
    1.16  val comp_ss = HOL_ss addsimps @{thms semiring_norm};
    1.17