Get untyped safety and determinism working for modules.

Also using a newer version of Lem that makes the spacing worse for the
generated HOL.  Hopefully this will be fixed soon.