diff -r b439582efc8a -r 43323d886ea3 src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Wed Jul 03 20:18:36 2024 +0200
+++ b/src/Pure/General/utf8.scala	Wed Jul 03 20:35:10 2024 +0200
@@ -23,7 +23,7 @@
   // see also https://en.wikipedia.org/wiki/UTF-8#Description
   // overlong encodings enable byte-stuffing of low-ASCII
 
-  def decode_permissive_bytes(bytes: Bytes.Vec): String = {
+  def decode_permissive(bytes: Bytes): String = {
     val size = bytes.size
     val buf = new java.lang.StringBuilder((size min Space.GiB(1).bytes).toInt)
     var code = -1
@@ -60,19 +60,4 @@
     flush()
     buf.toString
   }
-
-  def decode_permissive(text: String): String = {
-    val relevant = {
-      var i = 0
-      val n = text.length
-      var found = false
-      while (i < n && !found) {
-        if (text(i) >= 128) { found = true }
-        i += 1
-      }
-      found
-    }
-    if (relevant) decode_permissive_bytes(new Bytes.Vec_String(text))
-    else text
-  }
 }