# HG changeset patch
# User wenzelm
# Date 1124192552 -7200
# Node ID 1df7ad3a60827306ba5506380e4e6a7a4efd4813
# Parent  cca2f393844345f1ba57c4f152f9ef462f470558
tuned unsuffix/unprefix;

diff -r cca2f3938443 -r 1df7ad3a6082 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Aug 16 13:42:31 2005 +0200
+++ b/src/Pure/library.ML	Tue Aug 16 13:42:32 2005 +0200
@@ -843,16 +843,12 @@
 fun suffix sffx s = s ^ sffx;
 
 fun unsuffix sffx s =
-  let val m = size sffx; val n = size s - m in
-    if n >= 0 andalso String.substring (s, n, m) = sffx then String.substring (s, 0, n)
-    else raise Fail "unsuffix"
-  end;
+  if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
+  else raise Fail "unsuffix";
 
 fun unprefix prfx s =
-  let val m = size prfx; val n = size s - m in
-    if String.isPrefix prfx s then String.substring (s, m, n)
-    else raise Fail "unprefix"
-  end;
+  if String.isPrefix prfx s then String.substring (s, size prfx, size s - size prfx)
+  else raise Fail "unprefix";
 
 fun replicate_string 0 _ = ""
   | replicate_string 1 a = a