diff -r 715bf5beedc0 -r e29f47e04180 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Wed Mar 23 09:37:38 2016 +1100
+++ b/src/Pure/General/sha1.scala	Thu Mar 24 13:08:12 2016 +0100
@@ -36,6 +36,8 @@
     new Digest(result.toString)
   }
 
+  def fake(rep: String): Digest = new Digest(rep)
+
   def digest(file: JFile): Digest =
   {
     val stream = new FileInputStream(file)
@@ -63,9 +65,7 @@
   }
 
   def digest(bytes: Bytes): Digest = bytes.sha1_digest
-
   def digest(string: String): Digest = digest(Bytes(string))
 
-  def fake(rep: String): Digest = new Digest(rep)
+  val digest_length: Int = digest("").rep.length
 }
-