# 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 =