src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Mon Jul 08 22:28:02 2024 +0100
+++ b/src/Pure/General/symbol.scala	Tue Jul 09 12:32:33 2024 +0200
@@ -51,6 +51,7 @@
   def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
 
   def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
+  def is_ascii_digit(b: Byte): Boolean = is_ascii_digit(b.toChar)
 
   def is_ascii_hex(c: Char): Boolean =
     '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'