Dear Isabelle developers, When I am porting some of my old code from Isabelle-2016 to Isabelle2016-1, I have encountered a problem that the command “SML_file" does not accept a SML file that contains the function “PolyML.IntInf.gcd”. By going through NEWS, I found the following entry:
* Low-level ML system structures (like PolyML and RunCall) are no longer exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY. I am a little confused as I thought SML_file should accept Standard ML files (rather than Poly/ML ones). By the ways, both SML_file and ML_file in Isabelle2016 accept “PolyML.IntInf.gcd", while ML_file in Isabelle2016-1(and the development version) accept this command. This further confused me, as I thought ML_file is the command that compiles Poly/ML files and should reject “PolyML.IntInf.gcd” in Isabelle2016-1 as suggested by NEWS. Any help is greatly appreciated, Wenda _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
