In figure 2, rho (y) = <C, v> rho [z -> v], e hook [p] ------------------------------------------------ rho, case y of ... | C z => e | ... hook [p] seems to be missing (assuming the non-exception case doesn't handle this).