removed nospaces (Char.isSpace does not conform to Isabelle conventions);
authorwenzelm
Thu Dec 28 14:30:40 2006 +0100 (2006-12-28)
changeset 21920f1c096441023
parent 21919 b142e6506469
child 21921 f241e9cd26ca
removed nospaces (Char.isSpace does not conform to Isabelle conventions);
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Dec 28 14:30:39 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Dec 28 14:30:40 2006 +0100
     1.3 @@ -163,7 +163,6 @@
     1.4    val unsuffix: string -> string -> string
     1.5    val replicate_string: int -> string -> string
     1.6    val translate_string: (string -> string) -> string -> string
     1.7 -  val nospaces: string -> string
     1.8  
     1.9    (*lists as sets -- see also Pure/General/ord_list.ML*)
    1.10    val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
    1.11 @@ -808,8 +807,6 @@
    1.12        if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
    1.13        else replicate_string (k div 2) (a ^ a) ^ a;
    1.14  
    1.15 -val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c);
    1.16 -
    1.17  
    1.18  (** lists as sets -- see also Pure/General/ord_list.ML **)
    1.19