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).