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