Use [fill K] in tac_wp_pure

This is more consistent with other tac_wp tactics for HeapLang and also
a tiny bit more efficient, which is good to embody in the basic tactics
so derived code follows the same patterns.