src/HOL/Tools/Qelim/cooper.ML
changeset 27018 b3e63f39fc0f
parent 26928 ca87aff1ad2d
child 27330 1af2598b5f7d
     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 =