--- a/src/Pure/General/output.ML Sat Dec 15 13:08:30 2007 +0100
+++ b/src/Pure/General/output.ML Sat Dec 15 13:08:31 2007 +0100
@@ -31,7 +31,6 @@
val output_width: string -> output * int
val output: string -> output
val escape: output -> string
- val escape_malformed: string -> string
val std_output: output -> unit
val std_error: output -> unit
val immediate_output: string -> unit
@@ -74,7 +73,6 @@
val output = #1 o output_width;
fun escape x = #escape (get_mode ()) x;
-val escape_malformed = escape o translate_string output;