CakeML:87abd8d7c7dd2cefac8016fd4ad198bd3df677f6 Merge pull request #1437 from CakeML/whole_prog_thm [Jul 23 14:50:53] HOL:f18e6e7277c2648d40c2491d87f09083c909e6e9 OT logging: stop re-stripping already-undecorated retired names [Jul 19 03:05:49]