src/Pure/goals.ML

--- a/src/Pure/goals.ML	Thu Jan 14 14:39:11 1999 +0100
+++ b/src/Pure/goals.ML	Fri Jan 15 16:13:31 1999 +0100
@@ -309,9 +309,11 @@
 val current_goals_markers = ref ("", "", "");
 
 fun print_current_goals_default n max th =
-  let val ref (begin_state, end_state, begin_goal) = current_goals_markers in
-    if begin_state = "" then () else writeln begin_state;
-    writeln ("Level " ^ string_of_int n);
+  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 "") ^ ")");
     Locale.print_goals_marker begin_goal max th;
     if end_state = "" then () else writeln end_state
   end;