# HG changeset patch
# User nipkow
# Date 1237895101 -3600
# Node ID 48f5a5524e1180ef65d85e684f528bcd16fc7aeb
# Parent  226c91456e5435c0c2d1bb643b43fd7a64a57fae
presburger uses [arith] now

diff -r 226c91456e54 -r 48f5a5524e11 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Sun Mar 22 19:43:21 2009 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Tue Mar 24 12:45:01 2009 +0100
@@ -163,8 +163,10 @@
 
 fun cooper_tac elim add_ths del_ths ctxt =
 let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths
+    val aprems = ArithFacts.get ctxt
 in
-  ObjectLogic.full_atomize_tac
+  Method.insert_tac aprems
+  THEN_ALL_NEW ObjectLogic.full_atomize_tac
   THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   THEN_ALL_NEW simp_tac ss
   THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))