progress on compile_top_thm

up to re-establishing the invariant (in the first case), though there
have been cheats left behind.
fix bug with printing types

build_tdefs has acquired a REVERSE for some reason; the compiler needs
to print things in the same order as it.