rework various things to do with modules in compilerProofsScript.sml

had been getting FV_decs and decs_cns wrong: the semantics is that
bindings introduced in earlier declarations are no longer free in later
declarations. so these have to be fold-like rather than map-like.

this breaks some of the closedness proofs in replCorrect, which are now
cheated.