obsolete --- superseded by SHA1.Shasum operations;

--- a/src/Pure/General/sha1.scala	Mon Feb 06 16:04:17 2023 +0100
+++ b/src/Pure/General/sha1.scala	Mon Feb 06 16:11:05 2023 +0100
@@ -48,8 +48,6 @@
   def digest(bytes: Array[Byte]): Digest = make_digest(_.update(bytes))
   def digest(bytes: Bytes): Digest = bytes.sha1_digest
   def digest(string: String): Digest = digest(Bytes(string))
-  def digest_set(digests: List[Digest]): Digest =
-    digest(cat_lines(digests.map(_.toString).sorted))
 
   val digest_length: Int = digest("").toString.length