--- 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 **)