# HG changeset patch
# User wenzelm
# Date 918491526 -3600
# Node ID 0ebfcf181d8480445d3d0a3bbc0dfb7c913f01ed
# Parent  6dc692fb3d281b71c8a3a365ffd621d0d0ed745e
tuned msg;

diff -r 6dc692fb3d28 -r 0ebfcf181d84 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Feb 08 17:31:50 1999 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Feb 08 17:32:06 1999 +0100
@@ -275,10 +275,10 @@
       | levels_up i = " (" ^ string_of_int i ^ " levels up)";
 
     fun print_goal (i, ((kind, name, _, _), (_, thm))) =
-      (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 1) ^ ":"); (* FIXME *)
+      (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
         Locale.print_goals_marker begin_goal (! goals_limit) thm);
   in
-    writeln ("Nesting level: " ^ string_of_int (length nodes div 1));   (* FIXME *)
+    writeln ("Nesting level: " ^ string_of_int (length nodes div 2));
     writeln "";
     writeln (mode_name mode ^ " mode");
     writeln "";
diff -r 6dc692fb3d28 -r 0ebfcf181d84 src/Pure/Thy/session.ML
--- a/src/Pure/Thy/session.ML	Mon Feb 08 17:31:50 1999 +0100
+++ b/src/Pure/Thy/session.ML	Mon Feb 08 17:32:06 1999 +0100
@@ -42,7 +42,7 @@
 
 fun init reset parent name =
   if not (parent mem_string (! session)) orelse not (! session_finished) then
-    error ("Unfinished parent session " ^ quote (str_of (! session)) ^ " for " ^ quote name)
+    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
   else (add_path reset name; session_finished := false);