Minor cleanups in thm 7