diff -r 4fc8a35579b2 -r 5945c6f5126a src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Tue Jun 21 15:40:18 2022 +0200
+++ b/src/Pure/General/bytes.ML	Tue Jun 21 15:48:59 2022 +0200
@@ -19,6 +19,7 @@
   val empty: T
   val add_substring: substring -> T -> T
   val add: string -> T -> T
+  val append: T -> T -> T
   val build: (T -> T) -> T
   val string: string -> T
   val buffer: Buffer.T -> T
@@ -70,6 +71,11 @@
 
 end;
 
+fun append bytes1 bytes2 =  (*left-associative*)
+  if is_empty bytes1 then bytes2
+  else if is_empty bytes2 then bytes1
+  else bytes1 |> fold add (contents bytes2);
+
 fun build (f: T -> T) = f empty;
 
 val string = build o add;