# HG changeset patch
# User berghofe
# Date 1090253569 -7200
# Node ID 7b4abcfae4e10ab08c1bb06e4faf5697096bf9d9
# Parent  66ded85a6749f9128fd732b326aa03cbd5014603
Added function unprefix.

diff -r 66ded85a6749 -r 7b4abcfae4e1 src/Pure/library.ML
--- 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 =