CakeML:cc5246f4dc0a756dec2f25f552a213f3a96956e5 Delete some old junk #478 (trans-ind) Merging into:321cbf4ab8f49f1d20ae3252e62bccb48e0e2f1e Fix for new HOL pretty-printing infrastructure HOL:d35b02e22c3460109d55f5465673d0735657eb8b Restore ppstream_funs as nullary type operator in term_pp_types Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux Claimed job