Depends on [HOL#1597](https://github.com/HOL-Theorem-Prover/HOL/issues/1597) and [cake#1109](https://github.com/CakeML/cakeml/issues/1109).