src/HOL/Tools/Qelim/presburger.ML
changeset 27019 9ad9d6554d05
parent 25843 af0c90f54ebe
child 27651 16a26996c30e
--- a/src/HOL/Tools/Qelim/presburger.ML	Thu May 29 23:46:39 2008 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Thu May 29 23:46:40 2008 +0200
@@ -164,7 +164,7 @@
   (if q then I else TRY) (rtac TrueI i));
 
 fun cooper_tac elim add_ths del_ths ctxt =
-let val ss = fst (CooperData.get ctxt) delsimps del_ths addsimps add_ths
+let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths
 in
   ObjectLogic.full_atomize_tac
   THEN_ALL_NEW CONVERSION Thm.eta_long_conversion