# HG changeset patch
# User wenzelm
# Date 1212097599 -7200
# Node ID b3e63f39fc0f44ffd98c80f513caf142de8ac974
# Parent  1e0e8c1adf8c78c465de2bfd76b4f5d66d6eae4e
proper context for simp_thms_conv;

diff -r 1e0e8c1adf8c -r b3e63f39fc0f src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu May 29 23:46:37 2008 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu May 29 23:46:39 2008 +0200
@@ -16,7 +16,8 @@
 open Normalizer;
 
 exception COOPER of string * exn;
-val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
+fun simp_thms_conv ctxt =
+  Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps simp_thms);
 val FWD = Drule.implies_elim_list;
 
 val true_tm = @{cterm "True"};
@@ -491,7 +492,7 @@
    in [dp, inf, nb, pd] MRS cpth
    end
  val cpth' = Thm.transitive uth (cpth RS eq_reflection)
-in Thm.transitive cpth' ((simp_thms_conv then_conv eval_conv) (Thm.rhs_of cpth'))
+in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv) (Thm.rhs_of cpth'))
 end;
 
 fun literals_conv bops uops env cv =