src/Pure/General/sha1_polyml.ML

 implementation.
 *)
 
 structure SHA1: SHA1 =
 struct
+
+(* digesting *)
 
 fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
 
 fun hex_string arr i =
   let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)

       CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
         (CInterface.STRING, CInterface.LONG, 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
+fun digest_string str = digest_external str
   handle CInterface.Foreign msg =>
-    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.digest str);
+    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.rep (SHA1.digest str));
+
+
+(* type digest *)
+
+datatype digest = Digest of string;
+
+val digest = Digest o digest_string;
+fun rep (Digest s) = s;
 
 end;