clarified catch-all handler --- avoid confusion of Interrupt vs. Exn.Interrupt in varying ML contexts;