# HG changeset patch
# User wenzelm
# Date 931299306 -7200
# Node ID 6721243019e7bdb3d1a5bc04d72e198b2c1903cd
# Parent  ef0f25d0bc2d0ff15f3cd3538591bc94389c3c5e
tuned output;

diff -r ef0f25d0bc2d -r 6721243019e7 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue Jul 06 21:16:29 1999 +0200
+++ b/src/Pure/goals.ML	Wed Jul 07 00:15:06 1999 +0200
@@ -318,7 +318,7 @@
       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 "") ^ ")");
+	   (if ngoals <> 1 then "s" else "") ^ ")");
     Locale.print_goals_marker begin_goal max th;
     if end_state = "" then () else writeln end_state
   end;