diff -r 545d474ada44 -r e181259e539b src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Mon Nov 04 14:39:27 2024 +0100 +++ b/src/Pure/General/symbol.scala Mon Nov 04 14:50:21 2024 +0100 @@ -673,7 +673,9 @@ def apply(str: String): Double = (for (s <- iterator(str)) yield { val sym = encode(s) - if (sym.startsWith("\\