# HG changeset patch
# User wenzelm
# Date 933601144 -7200
# Node ID e9c253036b4548fa65e90f086349c07db32f5a80
# Parent  ff492d5d77cc9b95531dbc4ee4363e12f87b2dd2
removed obsolete concat;

diff -r ff492d5d77cc -r e9c253036b45 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Aug 02 11:33:18 1999 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Aug 02 15:39:04 1999 +0200
@@ -13,13 +13,12 @@
 
 
 structure String =
-  struct
+struct
   fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j)
                           handle Substring => raise Subscript
   fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
                        handle Subscript => false
-  val concat = implode
-  end;
+end;
 
 
 (** ML system related **)