rework compilation of declarations

Consider something like:

structure M = struct
val (x,y,z) = e1;
val (a,b) = e2;
end;
(suppose the pat_bindings for (x,y,z) is [x,y,z]. in reality the
semantics is reversed, though.)

The semantics says the environment at the end should have domain (in
order): a b x y z. (And my invariant wants the compiler's domain to
match the semantics exactly.)

My strategy here was to make the stack go like this:
handler
(x,y,z), handler
z, y, x, handler
(a,b), z, y, x, handler
b, a, z, y, x, handler
(x,y,z,a,b), handler
(x,y,z,a,b)
b, a, z, y, x

That's ended up in the wrong order, with no easy way out.  Also, since I
do printing in the last step, the results get printed in the wrong order
too. (I know we don't print anything for modules, but I want the proof
for this function to work for a list of top-level declarations all at
once. The bootstrap may include such a thing..)

Now, I do this instead (i.e. compile each declaration in reverse):
(z,y,x), handler
x, y, z, handler
(b,a), x, y, z, hanlder
a, b, x, y, z, handler
(z,y,x,b,a), handler
(z,y,x,b,a)
a, b, x, y, z

The proofs up to compile_decs_thm have been updated. Some of the
compiler tests were too discriminating - commented them out (the tests
shouldn't test the order of non-observable stuff on the stack).

The new proofs avoid the weird new_decs_renv constant for doing the
weird reverse-inside-reverse effect of cons-ing things at two levels.

Hopefully the proof of compile_decs_wrap_thm will now go through...