--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue Jul 28 18:59:15 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue Jul 28 19:49:54 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 (Thm.add_cterm_frees tm [])
+ val qe_conv = Qelim.gen_qelim_conv 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