# HG changeset patch
# User berghofe
# Date 1082133879 -7200
# Node ID ee0fb03f5f1e327e8566b22e124c5d94fd1d4a4b
# Parent  c36e116b578b770ccaf7d1525303b804b1a2c81a
Added translate function to String structure.

diff -r c36e116b578b -r ee0fb03f5f1e src/Pure/ML-Systems/polyml-3.x.ML
--- a/src/Pure/ML-Systems/polyml-3.x.ML	Fri Apr 16 18:43:36 2004 +0200
+++ b/src/Pure/ML-Systems/polyml-3.x.ML	Fri Apr 16 18:44:39 2004 +0200
@@ -18,6 +18,8 @@
                           handle Substring => raise Subscript
   fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
                        handle Subscript => false
+  fun str (s : string) = s;
+  fun translate f s = implode (map f (explode s));
 end;
 
 
diff -r c36e116b578b -r ee0fb03f5f1e src/Pure/ML-Systems/smlnj-0.93.ML
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Fri Apr 16 18:43:36 2004 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Fri Apr 16 18:44:39 2004 +0200
@@ -15,6 +15,8 @@
     handle String.Substring => raise Subscript;
   fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
     handle Subscript => false;
+  fun str (s : string) = s;
+  fun translate f s = implode (map f (explode s));
 end;