diff -r 0f86a8a694f8 -r d2baf4b79424 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Jun 12 22:45:59 2004 +0200
+++ b/src/Pure/library.ML	Sat Jun 12 22:46:21 2004 +0200
@@ -177,6 +177,7 @@
   val suffix: string -> string -> string
   val unsuffix: string -> string -> string
   val replicate_string: int -> string -> string
+  val translate_string: (string -> string) -> string -> string
 
   (*lists as sets*)
   val mem: ''a * ''a list -> bool
@@ -597,6 +598,8 @@
     else rep (n, [])
   end;
 
+fun translate_string f = String.translate (f o String.str);
+
 (*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
 fun multiply ([], _) = []
   | multiply (x :: xs, yss) = map (cons x) yss @ multiply (xs, yss);