src/HOL/Decision_Procs/ferrante_rackoff.ML

       (put_simpset HOL_basic_ss ctxt addsimps
         @{thms simp_thms ex_simps all_simps not_all all_not_ex ex_disj_distrib}), ss);
    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
                    then_conv postcv)
  in (Simplifier.rewrite (put_simpset ss ctxt) then_conv qe_conv) tm end;