# HG changeset patch
# User wenzelm
# Date 887794668 -3600
# Node ID 437ddddbfef5058290be04bd1612c68fad7767d6
# Parent  401dd9b1b5484feff7ca8d40c1d005892a7cb6ed
tuned comment;

diff -r 401dd9b1b548 -r 437ddddbfef5 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Feb 13 20:16:02 1998 +0100
+++ b/src/Pure/library.ML	Wed Feb 18 10:37:48 1998 +0100
@@ -616,7 +616,7 @@
   | is_quasi_letter ch = is_letter ch;
 
 (*white space: blanks, tabs, newlines, formfeeds*)
-val is_blank : string -> bool =
+val is_blank : string -> bool =					(* FIXME *)
   fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\160" => true
     | _ => false;