src/Pure/ML-Systems/polyml.ML
changeset 7147 ff492d5d77cc
parent 7114 f1e787b90fdc
child 7148 e9c253036b45
equal deleted inserted replaced
7146:3c664fbb2910 7147:ff492d5d77cc
    14 
    14 
    15 structure String =
    15 structure String =
    16   struct
    16   struct
    17   fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j)
    17   fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j)
    18                           handle Substring => raise Subscript
    18                           handle Substring => raise Subscript
       
    19   fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
       
    20                        handle Subscript => false
    19   val concat = implode
    21   val concat = implode
    20   end;
    22   end;
    21 
    23 
    22 
    24 
    23 (** ML system related **)
    25 (** ML system related **)