Isabelle is still a very active LCF proof assistant, and it's still written in Poly/ML. It's pretty aggressively concurrent under the bonnet, and leverages Poly/ML well for that. There's still HOL4, which predates Isabelle and is still going, and it also recommends using Poly/ML.
I mostly worked with HOL Light which started as a CAML project and now runs on OCaml.
I mostly worked with HOL Light which started as a CAML project and now runs on OCaml.