Because lisp is good at anything? But especially alternative evaluation systems (of which theorem proving is one).

Because they took lisp and added types to it; via the ISWIM language document ("The Next 700 Programming Languages") which was based off of the original lisp.

Because the lisp language family is a formulation of lambda calculus and has first class functions, unlike any other language family at the time, and that is necessary for theorem proving that is based on lambda calculus.

Because they likely prototyped the system in a set of lisp macros before writing the language (all the authors knew lisp and had taught each other it).

Can you point me to a good reference paper about this?

No one has really written a paper about the history of all this (I also mentioned this paper [1] in one of my other comments). But if you read the original ML paper [0] you'll see how they developed the language (notably by using ISWIM's syntax as a base). Note also that they are solving a problem with LISP (and dismissing Algol languages entirely) by building in strong types.

[0] http://www.sciencedirect.com/science/article/pii/00220000789...

[1] https://archive.alvb.in/msc/11_infomtpt/papers/the-next-700_...