changeset 5909 | 3fc6497f1c7b |
parent 5870 | 5d4fc952be47 |
--- a/src/Pure/Syntax/symbol.ML Tue Nov 17 14:08:46 1998 +0100 +++ b/src/Pure/Syntax/symbol.ML Tue Nov 17 14:09:00 1998 +0100 @@ -200,7 +200,7 @@ val is_letdig = is_quasi_letter orf is_digit; fun is_printable s = - size s = 1 andalso ord " " <= ord s andalso ord s <= ord "~" orelse + size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse size s > 2 andalso nth_elem (2, explode s) <> "^";