CakeML:a0080001db5d25a5b7c669b5ebd70acfca415632 Merge pull request #862 from CakeML/gh859 [Jul 07 20:46:42] HOL:8b0248d705162f895cc7228fd638fe1c7d74b600 Fix Unicode violation from 5184a58dae1 [Jul 04 06:34:10] Machine:oven3 Jul 08 07:26:24 Claimed job