let mk_fresh th k d = Fresh(th, k, d)