proper writeln of begin_state;

--- a/src/Pure/goals.ML	Wed Aug 18 20:39:41 1999 +0200
+++ b/src/Pure/goals.ML	Wed Aug 18 20:40:28 1999 +0200
@@ -319,9 +319,12 @@
 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;
-      val ngoals = nprems_of th in
-    writeln (begin_state ^ "Level " ^ string_of_int n ^
+  let
+    val ref (begin_state, end_state, begin_goal) = current_goals_markers;
+    val ngoals = nprems_of th;
+  in
+    if begin_state = "" then () else writeln begin_state;
+    writeln ("Level " ^ string_of_int n ^
       (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
         (if ngoals <> 1 then "s" else "") ^ ")"
       else ""));