# HG changeset patch
# User wenzelm
# Date 911308140 -3600
# Node ID 3fc6497f1c7bbd5a6132f4d9c054a9b712af453c
# Parent  79109d4aab60308ca4073c120d48d1122b4c70da
space;

diff -r 79109d4aab60 -r 3fc6497f1c7b src/Pure/Syntax/symbol.ML
--- 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) <> "^";