author | wenzelm |
Tue, 17 Nov 1998 14:09:00 +0100 | |
changeset 5909 | 3fc6497f1c7b |
parent 5908 | 79109d4aab60 |
child 5910 | 151ee1a5c09c |
--- 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) <> "^";