src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Thu Oct 23 18:00:28 2025 +0200
+++ b/src/Pure/General/symbol.scala	Thu Oct 23 20:09:14 2025 +0200
@@ -393,7 +393,7 @@
             case _ => err()
           }
         }
-        decl.split("\\s+").toList match {
+        Word.explode(decl) match {
           case sym :: props if sym.length > 1 && !is_malformed(sym) =>
             (sym, read_props(props))
           case _ => err()