--- 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;