author | wenzelm |
Sat, 08 Sep 2007 20:37:22 +0200 | |
changeset 24564 | 260a65fa2900 |
parent 24563 | f2edc70f8962 |
child 24565 | 08578e380a41 |
--- 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;