added old_symbol_source;
tuned;

--- a/src/Pure/Thy/latex.ML	Fri Feb 04 21:44:04 2000 +0100
+++ b/src/Pure/Thy/latex.ML	Fri Feb 04 21:44:38 2000 +0100
@@ -8,6 +8,7 @@
 signature LATEX =
 sig
   datatype token = Basic of OuterLex.token | Markup of string * string | Verbatim of string
+  val old_symbol_source: Symbol.symbol list -> string
   val token_source: token list -> string
   val theory_entry: string -> string
 end;
@@ -46,7 +47,8 @@
 
 in
 
-val output_syms = implode o map output_sym o Symbol.explode;
+val output_symbols = implode o map output_sym;
+val output_syms = output_symbols o Symbol.explode;
 
 end;
 
@@ -86,8 +88,10 @@
 
 (* theory presentation *)
 
-fun token_source toks =
-  "\\begin{isabellesimple}%\n" ^ output_tokens toks ^ "\\end{isabellesimple}\n";
+val isabelle_simple = enclose "\\begin{isabellesimple}%\n" "\\end{isabellesimple}%\n";
+
+val old_symbol_source = isabelle_simple o output_symbols;
+val token_source = isabelle_simple o output_tokens;
 
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
 

--- a/src/Pure/Thy/present.ML	Fri Feb 04 21:44:04 2000 +0100
+++ b/src/Pure/Thy/present.ML	Fri Feb 04 21:44:38 2000 +0100
@@ -16,11 +16,12 @@
   val init: bool -> string -> string list -> string -> Url.T option * bool -> unit
   val finish: unit -> unit
   val init_theory: string -> unit
-  val verbatim_source: string -> (unit -> string list) -> unit
+  val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
   type token
   val basic_token: OuterLex.token -> token
   val markup_token: string * string -> token
   val verbatim_token: string -> token
+  val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
   val token_source: string -> (unit -> token list) -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
   val result: string -> string -> thm -> unit
@@ -364,6 +365,9 @@
 val markup_token = Latex.Markup;
 val verbatim_token = Latex.Verbatim;
 
+fun old_symbol_source name mk_text =
+  with_session () (fn _ => add_tex_source name (Latex.old_symbol_source (mk_text ())));
+
 fun token_source name mk_toks =
   with_session () (fn _ => add_tex_source name (Latex.token_source (mk_toks ())));