added strip_blanks;

--- a/src/Pure/General/symbol.ML	Wed Jan 31 16:35:46 2001 +0100
+++ b/src/Pure/General/symbol.ML	Wed Jan 31 22:14:53 2001 +0100
@@ -28,6 +28,7 @@
   val is_symbolic: symbol -> bool
   val is_printable: symbol -> bool
   val length: symbol list -> int
+  val strip_blanks: string -> string
   val beginning: symbol list -> string
   val scan: string list -> symbol * string list
   val scanner: string -> (symbol list -> 'a * symbol list) -> symbol list -> 'a
@@ -115,6 +116,9 @@
       Some s' => if s' = "long" orelse s' = "Long" then 2 else 1
     | None => 1)) + n) (0, ss);
 
+fun strip_blanks s =
+  implode (#1 (Library.take_suffix is_blank (#2 (Library.take_prefix is_blank (explode s)))));
+
 
 (* beginning *)