changeset 6042 | 0ccde2f25dd6 |
parent 5813 | 4eea84a9427d |
child 6227 | 3198f547f8af |
--- a/src/Pure/ML-Systems/polyml.ML Mon Dec 28 16:49:31 1998 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Mon Dec 28 16:50:11 1998 +0100 @@ -12,6 +12,12 @@ use "basis.ML"; +structure String = + struct + fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j) + handle Substring => raise Subscript + end; + (** ML system related **)