proper context for simp_thms_conv;
authorwenzelm
Thu May 29 23:46:39 2008 +0200 (2008-05-29)
changeset 27018b3e63f39fc0f
parent 27017 1e0e8c1adf8c
child 27019 9ad9d6554d05
proper context for simp_thms_conv;
src/HOL/Tools/Qelim/cooper.ML
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu May 29 23:46:37 2008 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu May 29 23:46:39 2008 +0200
     1.3 @@ -16,7 +16,8 @@
     1.4  open Normalizer;
     1.5  
     1.6  exception COOPER of string * exn;
     1.7 -val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
     1.8 +fun simp_thms_conv ctxt =
     1.9 +  Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps simp_thms);
    1.10  val FWD = Drule.implies_elim_list;
    1.11  
    1.12  val true_tm = @{cterm "True"};
    1.13 @@ -491,7 +492,7 @@
    1.14     in [dp, inf, nb, pd] MRS cpth
    1.15     end
    1.16   val cpth' = Thm.transitive uth (cpth RS eq_reflection)
    1.17 -in Thm.transitive cpth' ((simp_thms_conv then_conv eval_conv) (Thm.rhs_of cpth'))
    1.18 +in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv) (Thm.rhs_of cpth'))
    1.19  end;
    1.20  
    1.21  fun literals_conv bops uops env cv =