# HG changeset patch
# User paulson
# Date 933150514 -7200
# Node ID f1e787b90fdc0a2604709fb60a185db5bbfd35e4
# Parent  ab79d9fa8d8ec1b734f29d3b10d213f81c1357ba
added String.concat

diff -r ab79d9fa8d8e -r f1e787b90fdc src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Wed Jul 28 10:28:08 1999 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Jul 28 10:28:34 1999 +0200
@@ -16,6 +16,7 @@
   struct
   fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j)
                           handle Substring => raise Subscript
+  val concat = implode
   end;