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";