If you are trying to get HOL4 working on a Raspberry Pi, you need to use MoscowML.
Poly/ML native compilation is not really supported for Raspberry Pi, and its bytecode interpreter performs worse than MoscowML's bytecode interpreter anyways.
I learned this after spending a few frustrating days trying to get PolyML to build HOL4, fruitlessly, then gave Mosml a shot (and it worked like a charm).
The things you learn...