# HG changeset patch # User wenzelm # Date 933601163 -7200 # Node ID d0c2168f77041eff6056062318b359feee4ef27f # Parent e9c253036b4548fa65e90f086349c07db32f5a80 provide String structure; diff -r e9c253036b45 -r d0c2168f7704 src/Pure/ML-Systems/smlnj-0.93.ML --- a/src/Pure/ML-Systems/smlnj-0.93.ML Mon Aug 02 15:39:04 1999 +0200 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML Mon Aug 02 15:39:23 1999 +0200 @@ -9,6 +9,15 @@ (*needs the Basis Library emulation*) use "basis.ML"; +structure String = +struct + fun substring args = String.substring args + handle String.Substring => raise Subscript; + fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1)) + handle Subscript => false; +end; + + (** ML system related **)