absolute lib_path relative to ML_HOME -- for improved robustness;
explicit warning if shared library failed to load;

--- a/src/Pure/General/sha1_polyml.ML	Thu Mar 11 15:33:45 2010 +0100
+++ b/src/Pure/General/sha1_polyml.ML	Thu Mar 11 16:56:22 2010 +0100
@@ -15,15 +15,21 @@
   let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
   in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
 
+val lib_path =
+  ("$ML_HOME/" ^ (if String.isSuffix "cygwin" ml_system then "sha1.dll" else "libsha1.so"))
+  |> Path.explode;
+
 fun digest_external str =
   let
     val digest = CInterface.alloc 20 CInterface.Cchar;
-    val _ = CInterface.call3 (CInterface.get_sym "sha1" "sha1_buffer")
-      (CInterface.STRING, CInterface.INT, CInterface.POINTER)
-      CInterface.POINTER (str, size str, CInterface.address digest);
+    val _ =
+      CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
+        (CInterface.STRING, CInterface.INT, CInterface.POINTER)
+        CInterface.POINTER (str, size str, CInterface.address digest);
   in fold (suffix o hex_string digest) (0 upto 19) "" end;
 
 fun digest str = digest_external str
-  handle CInterface.Foreign _ => SHA1.digest str;
+  handle CInterface.Foreign msg =>
+    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.digest str);
 
 end;