Added function unprefix.

--- a/src/Pure/library.ML	Sun Jul 18 12:01:08 2004 +0200
+++ b/src/Pure/library.ML	Mon Jul 19 18:12:49 2004 +0200
@@ -176,6 +176,7 @@
   val untabify: string list -> string list
   val suffix: string -> string -> string
   val unsuffix: string -> string -> string
+  val unprefix: string -> string -> string
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
 
@@ -840,6 +841,14 @@
     else raise LIST "unsuffix"
   end;
 
+(*remove prefix*)
+fun unprefix prfx s =
+  let val (prfx', sfx) = splitAt (size prfx, explode s)
+  in
+    if implode prfx' = prfx then implode sfx
+    else raise LIST "unprefix"
+  end;
+
 fun replicate_string 0 _ = ""
   | replicate_string 1 a = a
   | replicate_string k a =