# HG changeset patch
# User wenzelm
# Date 1212097600 -7200
# Node ID 9ad9d6554d05baaa510483132607d3e05baa0388
# Parent  b3e63f39fc0f44ffd98c80f513caf142de8ac974
proper context for ss;

diff -r b3e63f39fc0f -r 9ad9d6554d05 src/HOL/Tools/Qelim/presburger.ML
--- 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