src/Pure/Isar/proof.ML
changeset 6262 0ebfcf181d84
parent 6091 e3cdbd929a24
child 6404 2daaf2943c79
     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 "";