# HG changeset patch
# User wenzelm
# Date 979678437 -3600
# Node ID e34948f185419b90a31cc7552a2f083d4812c1ab
# Parent  f1209aff9517d5cf3dbc3a655f65371f29d40d1e
export plain_output;

diff -r f1209aff9517 -r e34948f18541 src/Pure/General/symbol.ML
--- 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!*)