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