tuned msg;
authorwenzelm
Mon Feb 08 17:32:06 1999 +0100 (1999-02-08)
changeset 62620ebfcf181d84
parent 6261 6dc692fb3d28
child 6263 f30d1e31b9df
tuned msg;
src/Pure/Isar/proof.ML
src/Pure/Thy/session.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Feb 08 17:31:50 1999 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Feb 08 17:32:06 1999 +0100
     1.3 @@ -275,10 +275,10 @@
     1.4        | levels_up i = " (" ^ string_of_int i ^ " levels up)";
     1.5  
     1.6      fun print_goal (i, ((kind, name, _, _), (_, thm))) =
     1.7 -      (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 1) ^ ":"); (* FIXME *)
     1.8 +      (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
     1.9          Locale.print_goals_marker begin_goal (! goals_limit) thm);
    1.10    in
    1.11 -    writeln ("Nesting level: " ^ string_of_int (length nodes div 1));   (* FIXME *)
    1.12 +    writeln ("Nesting level: " ^ string_of_int (length nodes div 2));
    1.13      writeln "";
    1.14      writeln (mode_name mode ^ " mode");
    1.15      writeln "";
     2.1 --- a/src/Pure/Thy/session.ML	Mon Feb 08 17:31:50 1999 +0100
     2.2 +++ b/src/Pure/Thy/session.ML	Mon Feb 08 17:32:06 1999 +0100
     2.3 @@ -42,7 +42,7 @@
     2.4  
     2.5  fun init reset parent name =
     2.6    if not (parent mem_string (! session)) orelse not (! session_finished) then
     2.7 -    error ("Unfinished parent session " ^ quote (str_of (! session)) ^ " for " ^ quote name)
     2.8 +    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
     2.9    else (add_path reset name; session_finished := false);
    2.10  
    2.11