# HG changeset patch
# User nipkow
# Date 1237896798 -3600
# Node ID 08760e217eb7729050f6e2213115c96bf122efc6
# Parent  7b09a2d9bcfcc3b62f37d1cf9480430d3577101d
fix

diff -r 7b09a2d9bcfc -r 08760e217eb7 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Tue Mar 24 12:45:23 2009 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Tue Mar 24 13:13:18 2009 +0100
@@ -163,7 +163,7 @@
 
 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
+    val aprems = Arith_Data.get_arith_facts ctxt
 in
   Method.insert_tac aprems
   THEN_ALL_NEW ObjectLogic.full_atomize_tac