export plain_output;

--- a/src/Pure/General/symbol.ML	Tue Jan 16 19:22:13 2001 +0100
+++ b/src/Pure/General/symbol.ML	Tue Jan 16 21:53:57 2001 +0100
@@ -38,6 +38,7 @@
   val isabelle_fontN: string
   val symbolsN: string
   val xsymbolsN: string
+  val plain_output: string -> string
   val output: string -> string
   val output_width: string -> string * real
 end;
@@ -353,6 +354,7 @@
   | Some f => f s);
 
 val output = #1 o output_width;
+val plain_output = #1 o default_output;
 
 
 (*final declarations of this structure!*)