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