# HG changeset patch
# User wenzelm
# Date 1373380371 -7200
# Node ID b04cbc49bdcfacd5b40d3be47632005dd2f9fa4b
# Parent  4e855c120f6acfb6ad9ea5bb60b504df27e99fed
tuned message;

diff -r 4e855c120f6a -r b04cbc49bdcf src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 09 13:24:17 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 09 16:32:51 2013 +0200
@@ -154,7 +154,9 @@
   | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
   | level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
 
-fun str_of_state (State (NONE, _)) = "at top level"
+fun str_of_state (State (NONE, SOME (Theory (Context.Theory thy, _)))) =
+      "at top level, result theory " ^ quote (Context.theory_name thy)
+  | str_of_state (State (NONE, _)) = "at top level"
   | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode"
   | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode"
   | str_of_state (State (SOME (Proof _), _)) = "in proof mode"