| changeset 4630 | 437ddddbfef5 |
| parent 4629 | 401dd9b1b548 |
| child 4692 | 748f4e365d14 |
--- 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;