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