# HG changeset patch
# User wenzelm
# Date 932669634 -7200
# Node ID 06ae685ca5a3fe2f0c47d9c877d879faba8b344b
# Parent  e992884b256d0bc09f42c5d0895cfabd430340cc
avoid '(0 subgoals)';

diff -r e992884b256d -r 06ae685ca5a3 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Jul 22 20:53:26 1999 +0200
+++ b/src/Pure/goals.ML	Thu Jul 22 20:53:54 1999 +0200
@@ -316,9 +316,10 @@
 fun print_current_goals_default n max th =
   let val ref (begin_state, end_state, begin_goal) = current_goals_markers;
       val ngoals = nprems_of th in
-    writeln (begin_state ^ "Level " ^ string_of_int n ^ 
-	" (" ^ string_of_int ngoals ^ " subgoal" ^ 
-	   (if ngoals <> 1 then "s" else "") ^ ")");
+    writeln (begin_state ^ "Level " ^ string_of_int n ^
+      (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
+        (if ngoals <> 1 then "s" else "") ^ ")"
+      else ""));
     Locale.print_goals_marker begin_goal max th;
     if end_state = "" then () else writeln end_state
   end;