diff -r 4e9d22dcd595 -r 81518b38b316 src/Pure/General/sha1.ML --- a/src/Pure/General/sha1.ML Fri Nov 06 13:43:49 2020 +0100 +++ b/src/Pure/General/sha1.ML Fri Nov 06 14:32:42 2020 +0100 @@ -148,10 +148,10 @@ val library_path = Path.explode ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so")); -fun library_call args = +val library_call = Foreign.buildCall3 (Foreign.getSymbol (Foreign.loadLibrary (File.platform_path library_path)) "sha1_buffer", - (Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer) args; + (Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer); fun with_memory n = Thread_Attributes.uninterruptible (fn restore_attributes => fn f =>