src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Tue Aug 29 16:30:07 2023 +0200
+++ b/src/Pure/General/symbol.scala	Tue Aug 29 16:39:29 2023 +0200
@@ -286,13 +286,13 @@
 
   /** defined symbols **/
 
-  object Argument extends Enumeration {
-    val none, cartouche, space_cartouche = Value
+  object Argument {
+    def unapply(s: String): Option[Argument] =
+      try { Some(valueOf(s)) }
+      catch { case _: IllegalArgumentException => None}
+  }
 
-    def unapply(s: String): Option[Value] =
-      try { Some(withName(s)) }
-      catch { case _: NoSuchElementException => None}
-  }
+  enum Argument { case none, cartouche, space_cartouche }
 
   object Entry {
     private val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
@@ -339,7 +339,7 @@
   class Entry private(
     val symbol: Symbol,
     val name: String,
-    val argument: Symbol.Argument.Value,
+    val argument: Symbol.Argument,
     val code: Option[Int],
     val font: Option[String],
     val groups: List[String],