replace PrintE instruction with handwritten printing routine

This breaks repl_fun_alt_proofScript.sml in ways I can't fix easily, so
I've added a cheat there.

This removes some of the cheats in replCorrectScript.sml.

The code replacing PrintE is partially verified. I cheat on the rest of
that proof, since it's tedious, and would be better solved by symbolic
evaluation if I could be bothered to make that work. (e.g. EVAL can't do
conditional rewrites, which makes working with records annoying, and it
probably needs a nice rewrite capturing the essence of
bc_fetch_next_addr.)