| changeset 74249 | 9d9e7ed01dbb |
| parent 74239 | 914a214e110e |
| child 74269 | f084d599bb44 |
--- a/src/HOL/Tools/Qelim/qelim.ML Mon Sep 06 13:49:36 2021 +0200 +++ b/src/HOL/Tools/Qelim/qelim.ML Mon Sep 06 14:05:22 2021 +0200 @@ -66,7 +66,7 @@ fun standard_qelim_conv ctxt atcv ncv qcv p = let val pcv = pcv ctxt - in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_frees_of p) atcv ncv qcv p end + in gen_qelim_conv ctxt pcv pcv pcv cons (Misc_Legacy.cterm_frees p) atcv ncv qcv p end end;