src/Pure/ML-Systems/polyml-old-basis.ML
changeset 24564 260a65fa2900
parent 23141 1f6b6a7314cf
equal deleted inserted replaced
24563:f2edc70f8962 24564:260a65fa2900
     7 structure String =
     7 structure String =
     8 struct
     8 struct
     9   fun isSuffix s1 s2 =
     9   fun isSuffix s1 s2 =
    10     let val n1 = size s1 and n2 = size s2
    10     let val n1 = size s1 and n2 = size s2
    11     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
    11     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
       
    12   fun isSubstring s1 s2 =
       
    13     String.isPrefix s1 s2 orelse
       
    14       size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); 
    12   open String;
    15   open String;
    13 end;
    16 end;
    14 
    17 
    15 structure Substring =
    18 structure Substring =
    16 struct
    19 struct