With Isabelle/42b92fa72a51 we are on a pre-release version of Poly/ML 5.7. David Matthews is about to converge to a release. There are various changes in the runtime system, and a few ones in the compiler (more PIDE markup). For example, local identifier scopes are visualized in the Isabelle/ML IDE as for the logical term language. Makarius