src/Pure/General/sha1.scala

--- a/src/Pure/General/sha1.scala	Wed Nov 18 21:34:13 2020 +0100
+++ b/src/Pure/General/sha1.scala	Wed Nov 18 21:39:55 2020 +0100
@@ -66,6 +66,8 @@
 
   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("").rep.length
 }