--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Sep 09 16:53:40 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Sep 09 17:20:41 2021 +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 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,