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 env = Cterms.list_set_rev (Misc_Legacy.cterm_frees tm)
+   val env = Cterms.list_set_rev (Cterms.build (Drule.add_frees_cterm tm))
    val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons env
                   (isolate_conv ctxt) nnf
                   (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
                                                whatis = whatis, simpset = ss}) vs
                    then_conv postcv)