ACL2-PC::RUN-INSTR-ON-GOAL

(macro) auxiliary to THEN
Major Section:  PROOF-CHECKER-COMMANDS

See documentation for then.