Hi,I've noticed that some of the functions from library.ML do not compile under the usual standard library. Eg, "use "library.ML" crashes with functions like "space_implode"
which have the wrong type, changing 'string' for 'char'. What standard sml library is Isabelle using? Thanks,Sean