In a program I had with similar problems, I switched the vector to an array and
manually replaced each element in the vector afer the loop was done with it.
Kind of ugly because it is a form of manual storage allocation, but really needed
in my case.
_______________________________________________
MLton mailing list
MLton@mlton.org
http://mlton.org/mailman/listinfo/mlton