# HG changeset patch
# User wenzelm
# Date 1167312640 -3600
# Node ID f1c0964410237595fe27398b1a7e375a7a46a7c2
# Parent  b142e6506469cd8a146006e1d6735c0e0f692b74
removed nospaces (Char.isSpace does not conform to Isabelle conventions);

diff -r b142e6506469 -r f1c096441023 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 **)