In the definition of Value (figure 2), what is the Exn summand? If it is just the exception type (NOT packets) then this doesn't seem to exist in the source language (we just made it a datatype, right)? If it is the packet thing, then hook always goes to a value, never the packet.