Remove some unnecessary “magic” invocations in HOLPP.sml

These are a remnant of some ancient black magic in the Moscow ML
implementation.