| changeset 74249 | 9d9e7ed01dbb |
| parent 74239 | 914a214e110e |
| child 74269 | f084d599bb44 |
| 74248:ea9f2cb22e50 | 74249:9d9e7ed01dbb |
|---|---|
64 |
64 |
65 in |
65 in |
66 |
66 |
67 fun standard_qelim_conv ctxt atcv ncv qcv p = |
67 fun standard_qelim_conv ctxt atcv ncv qcv p = |
68 let val pcv = pcv ctxt |
68 let val pcv = pcv ctxt |
69 in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_frees_of p) atcv ncv qcv p end |
69 in gen_qelim_conv ctxt pcv pcv pcv cons (Misc_Legacy.cterm_frees p) atcv ncv qcv p end |
70 |
70 |
71 end; |
71 end; |
72 |
72 |
73 end; |
73 end; |