# HG changeset patch
# User wenzelm
# Date 968172685 -7200
# Node ID 67cdb658e4226f1c90d9a5e5a26fbe0813f36a7f
# Parent  96138f29545ec2ca50958bc4fc67933b3a49b56f
tuned output of isabelle env;

diff -r 96138f29545e -r 67cdb658e422 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Tue Sep 05 18:50:52 2000 +0200
+++ b/src/Pure/Isar/isar_output.ML	Tue Sep 05 18:51:25 2000 +0200
@@ -271,7 +271,7 @@
 fun cond_display prt =
   if ! display then
     Pretty.string_of (Pretty.indent (! indent) prt)
-    |> enclose "%\n\\begin{isabelle}%\n" "%\n\\end{isabelle}%\n"
+    |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   else
     Pretty.str_of prt
     |> enclose "\\isa{" "}";