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;