diff -r 7ea69c26524b -r e3af424fdd1a src/Pure/General/value.scala
--- a/src/Pure/General/value.scala	Fri Jul 05 00:12:32 2024 +0200
+++ b/src/Pure/General/value.scala	Fri Jul 05 00:18:51 2024 +0200
@@ -21,6 +21,9 @@
   }
 
   object Nat {
+    def unapply(bs: Bytes): Option[scala.Int] =
+      if (bs.byte_iterator.forall(b => '0' <= b && b <= '9')) unapply(bs.text)
+      else None
     def unapply(s: java.lang.String): Option[scala.Int] =
       s match {
         case Int(n) if n >= 0 => Some(n)