# HG changeset patch
# User wenzelm
# Date 1430668347 -7200
# Node ID 79ad597fe699908cce0fed2554f1a52f71a18653
# Parent  523ec7e4b02283c9b5bbaf2dd45653cc3c22bd60
tuned output;

diff -r 523ec7e4b022 -r 79ad597fe699 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun May 03 17:41:54 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun May 03 17:52:27 2015 +0200
@@ -382,9 +382,9 @@
           val lthy = f thy;
           val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy);
           val _ =
-            if begin then
-              Output.state (Pretty.string_of (Pretty.chunks (Local_Theory.pretty lthy)))
-            else ();
+            (case Local_Theory.pretty lthy of
+              [] => ()
+            | prts => Output.state (Pretty.string_of (Pretty.chunks prts)));
         in Theory (gthy, SOME lthy) end
     | _ => raise UNDEF));