Job 407

CakeML:db24a6f06472e78be907bcb865a29db1a269052e
  Remove double inclusion of check_type_def success [Aug 07 16:56:23]
#507 (type-error-msg)
Merging into:1b5f8be3242a8a1d13d1289f21c06650fb5eb463
  Update translator for new length check [Aug 06 19:03:49]
HOL:8a08db2774a674929be0790353c5d303f44984ff
  Report problems with simple definitions better [Aug 07 06:58:43]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Aug 07 17:21:46 Claimed job
Aug 07 17:21:58 Building HOL
Aug 07 17:25:29 FAILED: building HOL