Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
proper context for ss;
authorwenzelm
Thu, 29 May 2008 23:46:40 +0200
changeset 270199ad9d6554d05
parent 27018 b3e63f39fc0f
child 27020 b5b8afc9fdcd
proper context for ss;
src/HOL/Tools/Qelim/presburger.ML file | annotate | diff | comparison | revisions 
     1.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Thu May 29 23:46:39 2008 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Thu May 29 23:46:40 2008 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4    (if q then I else TRY) (rtac TrueI i));
     1.5  
     1.6  fun cooper_tac elim add_ths del_ths ctxt =
     1.7 -let val ss = fst (CooperData.get ctxt) delsimps del_ths addsimps add_ths
     1.8 +let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths
     1.9  in
    1.10    ObjectLogic.full_atomize_tac
    1.11    THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
wneuper/isa