tuned unsuffix/unprefix;
authorwenzelm
Tue Aug 16 13:42:32 2005 +0200 (2005-08-16)
changeset 170611df7ad3a6082
parent 17060 cca2f3938443
child 17062 7272b45099c7
tuned unsuffix/unprefix;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Aug 16 13:42:31 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Aug 16 13:42:32 2005 +0200
     1.3 @@ -843,16 +843,12 @@
     1.4  fun suffix sffx s = s ^ sffx;
     1.5  
     1.6  fun unsuffix sffx s =
     1.7 -  let val m = size sffx; val n = size s - m in
     1.8 -    if n >= 0 andalso String.substring (s, n, m) = sffx then String.substring (s, 0, n)
     1.9 -    else raise Fail "unsuffix"
    1.10 -  end;
    1.11 +  if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
    1.12 +  else raise Fail "unsuffix";
    1.13  
    1.14  fun unprefix prfx s =
    1.15 -  let val m = size prfx; val n = size s - m in
    1.16 -    if String.isPrefix prfx s then String.substring (s, m, n)
    1.17 -    else raise Fail "unprefix"
    1.18 -  end;
    1.19 +  if String.isPrefix prfx s then String.substring (s, size prfx, size s - size prfx)
    1.20 +  else raise Fail "unprefix";
    1.21  
    1.22  fun replicate_string 0 _ = ""
    1.23    | replicate_string 1 a = a