| changeset 74269 | f084d599bb44 |
| parent 74249 | 9d9e7ed01dbb |
| child 74274 | 36f2c4a5c21b |
--- a/src/HOL/Tools/Qelim/qelim.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/HOL/Tools/Qelim/qelim.ML Thu Sep 09 14:50:26 2021 +0200 @@ -65,8 +65,10 @@ in fun standard_qelim_conv ctxt atcv ncv qcv p = - let val pcv = pcv ctxt - in gen_qelim_conv ctxt pcv pcv pcv cons (Misc_Legacy.cterm_frees p) atcv ncv qcv p end + let + val pcv = pcv ctxt + val env = Cterms.list_set_rev (Misc_Legacy.cterm_frees p) + in gen_qelim_conv ctxt pcv pcv pcv cons env atcv ncv qcv p end end;