# HG changeset patch
# User wenzelm
# Date 1189276642 -7200
# Node ID 260a65fa2900735a10913767a96d021b42646e4f
# Parent  f2edc70f896219c03ca90225f6e49df47850b304
added String.isSubstring;

diff -r f2edc70f8962 -r 260a65fa2900 src/Pure/ML-Systems/polyml-old-basis.ML
--- a/src/Pure/ML-Systems/polyml-old-basis.ML	Sat Sep 08 19:58:39 2007 +0200
+++ b/src/Pure/ML-Systems/polyml-old-basis.ML	Sat Sep 08 20:37:22 2007 +0200
@@ -9,6 +9,9 @@
   fun isSuffix s1 s2 =
     let val n1 = size s1 and n2 = size s2
     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
+  fun isSubstring s1 s2 =
+    String.isPrefix s1 s2 orelse
+      size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); 
   open String;
 end;