--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue Sep 01 17:25:36 2015 +0200
@@ -206,7 +206,7 @@
val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
val postcv = Simplifier.rewrite (put_simpset ss ctxt);
val nnf = K (nnf_conv ctxt then_conv postcv)
- val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Drule.cterm_add_frees tm [])
+ val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_add_frees tm [])
(isolate_conv ctxt) nnf
(fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
whatis = whatis, simpset = ss}) vs