THIS in doc comment substituted with incorrect name

[rmn30]

I updated to the recent Sail release and was pleased that doc comments in latex output are working again, but noticed a minor issue which is new. Sometimes THIS in a doc comment is substituted with an incorrect name. For example the CHERIoT sail contains:

function getCapLength(c) : Capability -> CapLen =
    let ('base, 'top) = getCapBounds(c) in {
        /* For valid capabilties we expect top >= base and hence
         * length >= 0 but representation does allow top < base in some
         * cases so might encounter on untagged capabilities. Here we just
         * pretend it is a 65-bit quantitiy and wrap.
         */
        assert (not(c.tag) | top >= base);
        (top - base) % pow2(cap_len_width)
    }

/*!
 * THIS(cap, addr, len) checks whether the capability cap includes the region
 * specified by addr and len. Specifically it checks whether
 * cap.base $\le$ addr AND addr + len $\le$ cap.top. Note that this definition
 * returns true if len is zero and addr $=$ cap.top.
 */
val inCapBounds  : (Capability, CapAddrBits, CapLen) -> bool
function inCapBounds (cap, addr, size) = ...

but in the generated latex THIS is substituted with getCapLength instead of inCapBounds! The bug is present in releases 0.18 and 0.19. Doc comments were not emitted at all in 0.17.x but this is now fixed, thanks!