# HG changeset patch
# User berghofe
# Date 1002732073 -7200
# Node ID 49c14348a42b8818a33e8dc3c9d1e766982caf74
# Parent  92706a69daccdf59de6afe2864bd0f60ae6ff598
Exported output_symbols.

diff -r 92706a69dacc -r 49c14348a42b src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Oct 10 18:40:46 2001 +0200
+++ b/src/Pure/Thy/latex.ML	Wed Oct 10 18:41:13 2001 +0200
@@ -8,6 +8,7 @@
 
 signature LATEX =
 sig
+  val output_symbols: Symbol.symbol list -> string
   datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
   val output_tokens: (token * string) list -> string
   val tex_trailer: string