provide String structure;

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