removed unused escape_malformed;
authorwenzelm
Sat, 15 Dec 2007 13:08:31 +0100
changeset 25640 1546ffd84986
parent 25639 f37e4ac90541
child 25641 615aecd485ad
removed unused escape_malformed;
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;