minor performance tuning;

--- a/src/Pure/General/bytes.scala	Tue Jun 11 16:39:53 2024 +0200
+++ b/src/Pure/General/bytes.scala	Tue Jun 11 16:48:20 2024 +0200
@@ -20,14 +20,12 @@
 object Bytes {
   val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
 
-  def apply(s: CharSequence): Bytes = {
-    val str = s.toString
-    if (str.isEmpty) empty
+  def apply(s: CharSequence): Bytes =
+    if (s.isEmpty) empty
     else {
-      val b = UTF8.bytes(str)
+      val b = UTF8.bytes(s.toString)
       new Bytes(b, 0, b.length)
     }
-  }
 
   def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length)