src/Pure/Syntax/pretty.ML

   val big_list: string -> T list -> T
   val string_of: T -> string
   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;
 
 functor PrettyFun(): PRETTY =

       | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
   in
     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 ***)
 
 val () = setmargin 80;