Change REPL constructor semantics

Now when a module raises an exception, all of its constructors are added
to the operational semantics' constructor environment, not just the
constructors whose type definitions were reached.  There are type
soundness theorems for doing the update either way.