the extension to continuation based contification

[Matthew Fluet]

> Gamma1 join Gamma2
> = { F -> K' | F \in dom(Gamma1) U dom(Gamma2),
>               K' = case(Gamma1(F),Gamma2(F))
>                      of (bot,bot) => bot
>                       | (bot,K) => K
>                       | (K,bot) => K
>                       | (K1,K2) => if K1 = K2 
>                                     then K1
>                                     else KF ("return to F continuation") } 

I guess you also need to change the contification condition.  A function F
would be contifiable if Gamma(F) = K and K <> KF (the return to F
continuation).