# HG changeset patch
# User chaieb
# Date 1183365800 -7200
# Node ID 123a45589e0a40c1b99a46397eaa5e15a70a95c8
# Parent  d52108dd4b6cec9e50209e1fc2600afbad9a9ad7
Generic QE need no Context anymore

diff -r d52108dd4b6c -r 123a45589e0a src/HOL/Tools/Qelim/ferrante_rackoff.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Mon Jul 02 10:43:19 2007 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Mon Jul 02 10:43:20 2007 +0200
@@ -212,7 +212,7 @@
               @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss))
     val postcv = Simplifier.rewrite ss
     val nnf = K (nnf_conv then_conv postcv)
-    val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Thm.add_cterm_frees tm []) 
+    val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm []) 
                   (isolate_conv ctxt) nnf
                   (fn vs => ferrack_conv (thy,{isolate_conv = isolate_conv ctxt, 
                                                whatis = whatis, simpset = simpset}) vs
diff -r d52108dd4b6c -r 123a45589e0a src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Mon Jul 02 10:43:19 2007 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Mon Jul 02 10:43:20 2007 +0200
@@ -8,10 +8,10 @@
 
 signature QELIM =
 sig
- val gen_qelim_conv: Proof.context -> conv -> conv -> conv ->
+ val gen_qelim_conv: conv -> conv -> conv ->
    (cterm -> 'a -> 'a) -> 'a -> ('a -> cterm -> thm) ->
    ('a -> conv) -> ('a -> cterm -> thm) -> conv
- val standard_qelim_conv: Proof.context -> (cterm list -> cterm -> thm) ->
+ val standard_qelim_conv: (cterm list -> cterm -> thm) ->
    (cterm list -> conv) -> (cterm list -> cterm -> thm) -> cterm -> thm
 end;
 
@@ -25,9 +25,8 @@
 
 val all_not_ex = mk_meta_eq @{thm "all_not_ex"};
 
-fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv =
+fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv =
  let
-  val thy = ProofContext.theory_of ctxt
   fun conv env p =
    case (term_of p) of
     Const(s,T)$_$_ => if domain_type T = HOLogic.boolT
@@ -63,7 +62,7 @@
                  (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
                      @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]);
 
-fun standard_qelim_conv ctxt atcv ncv qcv p =
-  gen_qelim_conv ctxt pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p;
+fun standard_qelim_conv atcv ncv qcv p =
+  gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p;
 
 end;