Adjust to provision of new option monad stuff in core HOL.

Will break if you are not running a HOL with commit 51adc5dfa2