src/Pure/General/sha1.scala

--- a/src/Pure/General/sha1.scala	Thu Nov 14 16:55:32 2013 +0100
+++ b/src/Pure/General/sha1.scala	Thu Nov 14 17:17:57 2013 +0100
@@ -56,6 +56,8 @@
     make_result(digest)
   }
 
-  def digest(string: String): Digest = digest(UTF8.string_bytes(string))
+  def digest(bytes: Bytes): Digest = bytes.sha1_digest
+
+  def digest(string: String): Digest = digest(Bytes(string))
 }