LEFT-hand version recommended.

If the whole object is a proof term wrapped in

Proof of [thm name] (No object specified)

<pf term>

Store ML commands at the point into the first ML object at which all the globals needed have been defined. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html