Added translate function to String structure.

--- 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;
 
 

--- 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;