Fixups to the replacement std. lib for trunk

proof_admitted is used for the [admit] tactic, and we now are required
to declare ML Modules to get the standard tactics.