bit of progress on second case of compile_top_thm

but it turns out the statement/implementation is wrong: the
top_to_i1_correct theorem needs us to use the old "tops" in the case of
an exception.