finish updating first case of compile_top_thm
second case of compile_top_thm, and factor out some shared tactics
finish updating compile_top_thm