bit more compile_top_thm

cheating something about extending the exh, not sure the right way to
solve it