| changeset 74239 | 914a214e110e |
| parent 70159 | 57503fe1b0ff |
| child 74249 | 9d9e7ed01dbb |
--- a/src/HOL/Tools/Qelim/qelim.ML Sun Sep 05 19:47:06 2021 +0200 +++ b/src/HOL/Tools/Qelim/qelim.ML Sun Sep 05 21:09:31 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_add_frees p []) atcv ncv qcv p end + in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_frees_of p) atcv ncv qcv p end end;