added map_strs: (string -> string) -> T -> T;

--- a/src/Pure/Syntax/pretty.ML	Fri Aug 19 15:36:23 1994 +0200
+++ b/src/Pure/Syntax/pretty.ML	Fri Aug 19 15:36:45 1994 +0200
@@ -45,6 +45,7 @@
   val writeln: T -> unit
   val str_of: T -> string
   val pprint: T -> pprint_args -> unit
+  val map_strs: (string -> string) -> T -> T
   val setdepth: int -> unit
   val setmargin: int -> unit
 end;
@@ -228,6 +229,11 @@
     pp (prune (! depth) prt)
   end;
 
+(*Map strings*)
+fun map_strs f (Block (prts, ind, _)) = blk (ind, map (map_strs f) prts)
+  | map_strs f (String s) = String (f s)
+  | map_strs _ brk = brk;
+
 
 (*** Initialization ***)