I figured this out. The clue was from the SubstInNode, which SANY uses to wrap expressions from modules imported using INSTANCE/WITH with substitutions, so the substitutions are lazily applied instead of directly written. As the name suggests then, APSubstInNode is when the same thing happens to an ASSUME/PROVE block. I don't know why the substitution isn't just distributed over ASSUME/PROVE to affect the expressions within, but whatever; this spec will produce an XML export containing an APSubstInNode instance at the M!ap usage point:
---- MODULE Test ----
---- MODULE Inner ----
CONSTANT C
THEOREM ap == ASSUME C PROVE C
====
M == INSTANCE Inner WITH C <- TRUE
THEOREM M!ap
====
This does not appear in the tlaplus/examples, nor any other TLA+ spec floating around that I can find, so it's a pretty obscure feature that is essentially never exercised. Possibly some bugs lurking within.
Andrew Helwer