# HG changeset patch
# User wenzelm
# Date 1384808768 -3600
# Node ID 7a92ed889da418b8d6893b056d0ab5227df98244
# Parent  1fd24c96ce9bf381ca12f7efe7a8d77529725bf2
persistent value;

diff -r 1fd24c96ce9b -r 7a92ed889da4 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Mon Nov 18 19:56:34 2013 +0100
+++ b/src/Pure/General/bytes.scala	Mon Nov 18 22:06:08 2013 +0100
@@ -89,7 +89,7 @@
 
   /* content */
 
-  def sha1_digest: SHA1.Digest = SHA1.digest(bytes)
+  lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
   override def toString: String =
     UTF8.decode_chars(s => s, bytes, offset, offset + length).toString