# HG changeset patch # User wenzelm # Date 1729951651 -7200 # Node ID 6eccae3387706b101eab124edeed4aea0fc6785c # Parent a477ce2fe491bbfe03c75561f30c39fb199b4f58 more accurate Symbol.length; diff -r a477ce2fe491 -r 6eccae338770 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Sat Oct 26 16:07:03 2024 +0200 +++ b/src/Pure/General/symbol.ML Sat Oct 26 16:07:31 2024 +0200 @@ -501,7 +501,9 @@ (* length *) fun sym_len s = - if String.isPrefix "\092