tuned;

--- a/src/Pure/Thy/latex.ML	Mon Jun 26 00:00:40 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Jun 26 00:23:17 2000 +0200
@@ -104,7 +104,7 @@
   \%%% Local Variables:\n\
   \%%% mode: latex\n\
   \%%% TeX-master: \"root\"\n\
-  \%%% End:\n%";
+  \%%% End:\n";
 
 fun old_symbol_source name syms =
   isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);