# HG changeset patch
# User paulson
# Date 914860211 -3600
# Node ID 0ccde2f25dd65ecb880cc743aab8d7899e58ee8b
# Parent  684ec6a1d8028414478bb27ff9a18502d1463bb8
Basis Library compatible substring oeration

diff -r 684ec6a1d802 -r 0ccde2f25dd6 src/Pure/ML-Systems/polyml.ML
--- 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 **)