# HG changeset patch
# User wenzelm
# Date 865348738 -7200
# Node ID e31ac367387eae9f2e57054b31a3adb3a48a0103
# Parent  d0d86b96aa9693ef64578109ba5bfb1c07663f56
is_blank: fixed space2;

diff -r d0d86b96aa96 -r e31ac367387e src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jun 03 12:03:38 1997 +0200
+++ b/src/Pure/library.ML	Tue Jun 03 16:38:58 1997 +0200
@@ -391,7 +391,7 @@
 
 (*white space: blanks, tabs, newlines, formfeeds*)
 val is_blank : string -> bool =
-  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "160" => true
+  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\160" => true
     | _ => false;
 
 val is_letdig = is_quasi_letter orf is_digit;