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