prove compile_print_top_thm for the new printer

surprisingly complex proof: I guess because it essentially implements an
If-expression in bytecode (on whether to print an exception or not).