diff -r 12c3fe42b2a8 -r 2acdbb6ee521 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Apr 01 18:36:58 2020 +0200
+++ b/src/Pure/General/symbol.ML	Wed Apr 01 20:17:23 2020 +0200
@@ -501,10 +501,9 @@
 (* length *)
 
 fun sym_len s =
-  if not (is_printable s) then (0: int)
-  else if String.isPrefix "\092<long" s then 2
-  else if String.isPrefix "\092<Long" s then 2
-  else 1;
+  if String.isPrefix "\092<long" s orelse String.isPrefix "\092<Long" s then 2
+  else if is_printable s then 1
+  else 0;
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;