diff -r 2e7d7ec7a268 -r 45a3dc4688bc src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Thu Jul 14 19:28:17 2005 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Jul 14 19:28:18 2005 +0200
@@ -28,12 +28,6 @@
 (*-----------------------------------------------------------------*)
 
 
-(* Invoking the oracle *)
-
-fun pres_oracle sg t = 
-  invoke_oracle (theory "Presburger") "presburger_oracle" 
-     (sg, CooperDec.COOPER_ORACLE t) ;
-
 val presburger_ss = simpset_of (theory "Presburger");
 
 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
@@ -279,7 +273,7 @@
     let val pth = 
           (* If quick_and_dirty then run without proof generation as oracle*)
              if !quick_and_dirty 
-             then pres_oracle sg (Pattern.eta_long [] t1)
+             then presburger_oracle sg (Pattern.eta_long [] t1)
 (*
 assume (cterm_of sg 
 	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))