Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper context for ss;
authorwenzelm
Thu, 29 May 2008 23:46:40 +0200
changeset 27019 9ad9d6554d05
parent 27018 b3e63f39fc0f
child 27020 b5b8afc9fdcd
proper context for ss;
src/HOL/Tools/Qelim/presburger.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle