more accurate Symbol.length;

--- 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<long" s orelse String.isPrefix "\092<Long" s then 2
+  if String.isPrefix "\092<longlonglong" s then 4
+  else if String.isPrefix "\092<longlong" s then 3
+  else if String.isPrefix "\092<long" s orelse String.isPrefix "\092<Long" s then 2
   else if is_printable s then 1
   else 0;