# HG changeset patch
# User wenzelm
# Date 1458821292 -3600
# Node ID e29f47e04180c22c924fe68786cf400be523976f
# Parent  715bf5beedc060bb8b27877185cc88c8e7467e5c
tuned signature;

diff -r 715bf5beedc0 -r e29f47e04180 src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Wed Mar 23 09:37:38 2016 +1100
+++ b/src/Pure/General/sha1.ML	Thu Mar 24 13:08:12 2016 +0100
@@ -8,9 +8,9 @@
 signature SHA1 =
 sig
   eqtype digest
-  val digest: string -> digest
   val rep: digest -> string
   val fake: string -> digest
+  val digest: string -> digest
   val test_samples: unit -> unit
 end;
 
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
 }
-