# HG changeset patch
# User wenzelm
# Date 1675695049 -3600
# Node ID a7c4510ae251dc036c6d1c224663571d13467d2b
# Parent  a917f580a10705e13523b7fb9619e8cca4af9318
tuned --- implicit split;

diff -r a917f580a107 -r a7c4510ae251 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Mon Feb 06 15:46:27 2023 +0100
+++ b/src/Pure/General/sha1.scala	Mon Feb 06 15:50:49 2023 +0100
@@ -83,5 +83,5 @@
   def shasum(digest: Digest, name: String): Shasum = new Shasum(List(digest.toString + " " + name))
   def shasum_meta_info(digest: Digest): Shasum = shasum(digest, isabelle.setup.Build.META_INFO)
   def shasum_sorted(args: List[(Digest, String)]): Shasum =
-    flat_shasum(args.sortBy(_._2).map(arg => shasum(arg._1, arg._2)))
+    flat_shasum(args.sortBy(_._2).map(shasum))
 }