author | wenzelm |
Mon, 02 Aug 1999 15:39:04 +0200 | |
changeset 7148 | e9c253036b45 |
parent 7147 | ff492d5d77cc |
child 7149 | d0c2168f7704 |
--- a/src/Pure/ML-Systems/polyml.ML Mon Aug 02 11:33:18 1999 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Mon Aug 02 15:39:04 1999 +0200 @@ -13,13 +13,12 @@ structure String = - struct +struct fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j) handle Substring => raise Subscript fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1)) handle Subscript => false - val concat = implode - end; +end; (** ML system related **)