diff -r f33d37c171a9 -r da4e82434985 src/Pure/General/uuid.scala
--- a/src/Pure/General/uuid.scala	Sat Feb 24 10:55:16 2024 +0100
+++ b/src/Pure/General/uuid.scala	Sat Feb 24 11:05:11 2024 +0100
@@ -11,6 +11,7 @@
   type T = java.util.UUID
 
   def random(): T = java.util.UUID.randomUUID()
+  def random_string(): String = random().toString
 
   def unapply(s: String): Option[T] =
     try { Some(java.util.UUID.fromString(s)) }