Insert the ABS or DISP named by the text at the point. This is like keying in the text immediately after keying in `;'. If you've got a pointer to an ABS, you don't have to re-enter its name to insert it-- just `;;' on it.
E.g., entering `;;' on lambda has the same effect as entering `;lambda' on a slot, namely, insert [var].<*>

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html