# HG changeset patch
# User wenzelm
# Date 999972373 -7200
# Node ID 8e07689296621b9fd7f1b87a31e0d2d71935383d
# Parent  07a9d5db83217186e333a9f21a10edce8a7a2fe3
print_state: subgoals;

diff -r 07a9d5db8321 -r 8e0768929662 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Sep 08 20:05:32 2001 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Sep 08 20:06:13 2001 +0200
@@ -333,11 +333,16 @@
       | levels_up 1 = ", 1 level up"
       | levels_up i = ", " ^ string_of_int i ^ " levels up";
 
+    fun subgoals 0 = ""
+      | subgoals 1 = ", 1 subgoal"
+      | subgoals n = ", " ^ string_of_int n ^ " subgoals";
+      
     fun pretty_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
       pretty_facts "using "
         (if mode <> Backward orelse null goal_facts then None else Some goal_facts) @
-      [Pretty.str ("goal (" ^ kind_name kind ^ (if name = "" then "" else " " ^ name) ^
-        levels_up (i div 2) ^ "):")] @
+      [Pretty.str ("goal (" ^ kind_name kind ^
+          (if name = "" then "" else " " ^ name) ^
+            levels_up (i div 2) ^ subgoals (Thm.nprems_of thm) ^ "):")] @
       Locale.pretty_goals_marker begin_goal (! goals_limit) thm;
 
     val ctxt_prts =