diff -r 05a4ce3f6b0c -r df8d71edbc79 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Mon Feb 06 15:53:58 2023 +0100
+++ b/src/Pure/General/sha1.scala	Mon Feb 06 16:04:17 2023 +0100
@@ -67,6 +67,8 @@
 
     def is_empty: Boolean = rep.isEmpty
 
+    def :::(other: Shasum): Shasum = new Shasum(other.rep ::: rep)
+
     def digest: Digest = {
       rep match {
         case List(s)