# 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 **)