[MLton] it is necessary to manually make things tail-recursive?

[Stephen Weeks]

> If so, I can avoid rewriting everything in HOL to be tail-recursive
> and just rest safe in the knowledge that when I port to MLton all that
> code will be OK anyway.  

Yes.

The tradeoff between tail style and nontail style is between
heap-allocated closure records and stack-allocated stack frames.  Up
to a small constant factor, the same amount of stuff will be allocated
and live with both styles.  As Matthew said, MLton allocates the stack
on the heap and doubles it as necessary, so the only way to blow out
the stack is to run out of memory (unlike the ML Kit and Moscow ML).

As to which style is faster, it depends on the use.  I wouldn't spend
time rewriting your code without profiling and benchmarking.