(apply) Attempt to regenerate a proof term from the top goal and the tree of tactics. If there is no change to the proof, then fail. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html