| changeset 24593 | 1547ea587f5a |
| parent 24580 | 916259859344 |
| child 25521 | 6cebd2ff3ab7 |
--- a/src/Pure/General/symbol.ML Sat Sep 15 19:29:29 2007 +0200 +++ b/src/Pure/General/symbol.ML Sun Sep 16 14:52:26 2007 +0200 @@ -499,7 +499,7 @@ val xsymbolsN = "xsymbols"; fun sym_len s = - if not (is_printable s) then 0 + if not (is_printable s) then (0: int) else if String.isPrefix "\\<long" s then 2 else if String.isPrefix "\\<Long" s then 2 else if s = "\\<spacespace>" then 2