# HG changeset patch
# User wenzelm
# Date 953307045 -3600
# Node ID 8958ece3bbdfcdbf1bb7ea05792662a06251cd1b
# Parent  e16d6b54332e00df24d0d6134177830154118e58
old_symbol_source: include header;

diff -r e16d6b54332e -r 8958ece3bbdf src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Mar 17 16:30:03 2000 +0100
+++ b/src/Pure/Thy/latex.ML	Fri Mar 17 16:30:45 2000 +0100
@@ -8,7 +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 old_symbol_source: string -> Symbol.symbol list -> string
   val token_source: token list -> string
   val theory_entry: string -> string
 end;
@@ -90,7 +90,9 @@
 
 val isabelle_env = enclose "\\begin{isabelle}%\n" "\\end{isabelle}%\n";
 
-val old_symbol_source = isabelle_env o output_symbols;
+fun old_symbol_source name syms =
+  isabelle_env ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
+
 val token_source = isabelle_env o output_tokens;
 
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
diff -r e16d6b54332e -r 8958ece3bbdf src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Mar 17 16:30:03 2000 +0100
+++ b/src/Pure/Thy/present.ML	Fri Mar 17 16:30:45 2000 +0100
@@ -372,7 +372,7 @@
 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 ())));
+  with_session () (fn _ => add_tex_source name (Latex.old_symbol_source name (mk_text ())));
 
 fun token_source name mk_toks =
   with_session () (fn _ => add_tex_source name (Latex.token_source (mk_toks ())));