--- 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))