Fix a script that became broken with some recent changes to HOL.

This probably makes the script not work on older versions of HOL :(