--- a/src/Pure/General/value.scala	Mon Jul 08 22:28:02 2024 +0100
+++ b/src/Pure/General/value.scala	Tue Jul 09 12:32:33 2024 +0200
@@ -22,7 +22,7 @@
 
   object Nat {
     def unapply(bs: Bytes): Option[scala.Int] =
-      if (bs.byte_iterator.forall(b => '0' <= b && b <= '9')) unapply(bs.text)
+      if (bs.byte_iterator.forall(Symbol.is_ascii_digit)) unapply(bs.text)
       else None
     def unapply(s: java.lang.String): Option[scala.Int] =
       s match {