prove compile_print_top_thm and attempt to progress

but the printer implementation is wrong: it assumes the values to print
are exploded on the top of the stack, but the new front-end instead just
puts a NONE at the top of the stack (and the values are already in the
globals). since we can detect exceptions at this level, we should
probably print the "raise ..." in the exception case with a new printer
too.