author | wenzelm |
Tue, 10 Mar 1998 14:27:44 +0100 | |
changeset 4715 | 245d70532eed |
parent 4714 | bcdf68c78e18 |
child 4716 | a291e858061c |
--- a/src/Pure/Syntax/symbol.ML Tue Mar 10 13:27:13 1998 +0100 +++ b/src/Pure/Syntax/symbol.ML Tue Mar 10 14:27:44 1998 +0100 @@ -183,7 +183,8 @@ | is_quasi_letter s = is_letter s; val is_blank = - fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\\<space2>" => true + fn " " => true | "\t" => true | "\n" => true | "\^L" => true + | "\160" => true | "\\<space2>" => true | _ => false; val is_letdig = is_quasi_letter orf is_digit;