is_blank: added space2 (160);
authorwenzelm
Tue, 29 Apr 1997 16:38:16 +0200
changeset 3063 963e3bf01799
parent 3062 be354f68d340
child 3064 f04f93e5c0a9
is_blank: added space2 (160);
src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Apr 25 18:11:22 1997 +0200
+++ b/src/Pure/library.ML	Tue Apr 29 16:38:16 1997 +0200
@@ -390,7 +390,8 @@
 
 (*white space: blanks, tabs, newlines, formfeeds*)
 val is_blank : string -> bool =
-  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | _ => false;
+  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "160" => true
+    | _ => false;
 
 val is_letdig = is_quasi_letter orf is_digit;