equal
deleted
inserted
replaced
63 fun pcv ctxt = Simplifier.rewrite (put_simpset ss ctxt) |
63 fun pcv ctxt = Simplifier.rewrite (put_simpset ss ctxt) |
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 |
69 in gen_qelim_conv ctxt pcv pcv pcv cons (Misc_Legacy.cterm_frees p) atcv ncv qcv p end |
69 val pcv = pcv ctxt |
|
70 val env = Cterms.list_set_rev (Misc_Legacy.cterm_frees p) |
|
71 in gen_qelim_conv ctxt pcv pcv pcv cons env atcv ncv qcv p end |
70 |
72 |
71 end; |
73 end; |
72 |
74 |
73 end; |
75 end; |