diff -r afaa031ed4da -r 105519771c67 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Wed Sep 14 10:24:39 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Wed Sep 14 17:25:52 2005 +0200
@@ -44,7 +44,6 @@
   val evalc : term -> term
   val cooper_w : string list -> term -> (term option * term)
   val integer_qelim : Term.term -> Term.term
-  val presburger_oracle : theory -> term -> term
 end;
 
 structure  CooperDec : COOPER_DEC =
@@ -938,8 +937,4 @@
 
 val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; 
 
-fun presburger_oracle thy t =
-    if (!quick_and_dirty) 
-    then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t))
-    else error "Presburger oracle: not in quick_and_dirty mode"
 end;