# HG changeset patch
# User wenzelm
# Date 1197720511 -3600
# Node ID 1546ffd849869f3d204af9a294b7598f6bb2aa0f
# Parent  f37e4ac90541ffabf48c1315d8856e0795e70980
removed unused escape_malformed;

diff -r f37e4ac90541 -r 1546ffd84986 src/Pure/General/output.ML
--- 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;