src/Pure/General/pretty.ML

--- a/src/Pure/General/pretty.ML	Tue Sep 25 18:24:49 2012 +0200
+++ b/src/Pure/General/pretty.ML	Tue Sep 25 20:28:47 2012 +0200
@@ -61,6 +61,7 @@
   val output: int option -> T -> Output.output
   val string_of_margin: int -> T -> string
   val string_of: T -> string
+  val symbolic_string_of: T -> string
   val str_of: T -> string
   val writeln: T -> unit
   val to_ML: T -> ML_Pretty.pretty
@@ -324,6 +325,7 @@
 val output = Buffer.content oo output_buffer;
 fun string_of_margin margin = Output.escape o output (SOME margin);
 val string_of = Output.escape o output NONE;
+val symbolic_string_of = Output.escape o Buffer.content o symbolic;
 val str_of = Output.escape o Buffer.content o unformatted;
 val writeln = Output.writeln o string_of;