| changeset 60818 | 5e11a6e2b044 |
| parent 60801 | 7664e0916eec |
| child 61075 | f6b0d827240e |
--- a/src/HOL/Tools/Qelim/qelim.ML Tue Jul 28 18:59:15 2015 +0200 +++ b/src/HOL/Tools/Qelim/qelim.ML Tue Jul 28 19:49:54 2015 +0200 @@ -65,7 +65,7 @@ fun standard_qelim_conv ctxt atcv ncv qcv p = let val pcv = pcv ctxt - in gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p end + in gen_qelim_conv pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end end;