change definition of compile_decs to not do a case split

the cases (Dtype vs other) don't actually differ in a way that requires
a split: they just have empty stuff wherever the other case has
something.  straight line code should lead to a nicer proof.