diff -r 8e48a19fc81e -r 067c25edd1bd src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Aug 28 20:32:38 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Aug 28 20:32:55 2000 +0200
@@ -10,6 +10,7 @@
 sig
   datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
   val output_tokens: (token * string) list -> string
+  val tex_trailer: string
   val isabelle_file: string -> string
   val old_symbol_source: string -> Symbol.symbol list -> string
   val theory_entry: string -> string
@@ -117,14 +118,15 @@
 
 (* theory presentation *)
 
-val isabelle_file = enclose
-  "\\begin{isabelle}%\n"
-  "\\end{isabelle}%\n\
-  \%%% Local Variables:\n\
+val tex_trailer =
+  "%%% Local Variables:\n\
   \%%% mode: latex\n\
   \%%% TeX-master: \"root\"\n\
   \%%% End:\n";
 
+val isabelle_file =
+  enclose "%\n\\begin{isabellebody}%\n" ("\\end{isabellebody}%\n" ^ tex_trailer);
+
 fun old_symbol_source name syms =
   isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);