ml_hol_kernel builds, definitions made suitable for ML