# HG changeset patch
# User wenzelm
# Date 1005604129 -3600
# Node ID 74f92a43bac3441b50dcd61ad9c8796da5cc9308
# Parent  5fc22b8c03e912e0c52be46d295e25e325bec9f0
empty rule_context for multiple goals;

diff -r 5fc22b8c03e9 -r 74f92a43bac3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Nov 12 23:28:15 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 12 23:28:49 2001 +0100
@@ -342,7 +342,7 @@
       | subgoals n = ", " ^ string_of_int n ^ " subgoals";
 
     fun prt_names names =
-      (case filter_out (equal "") names of [] => "" | nms => space_implode " and " nms);
+      (case filter_out (equal "") names of [] => "" | nms => " " ^ space_implode " and " nms);
 
     fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) =
       pretty_facts "using " ctxt
@@ -632,7 +632,9 @@
     state'
     |> map_context (autofix props)
     |> put_goal (Some (((kind, names, propss), ([], goal)), after_qed o map_context gen_binds))
-    |> map_context (ProofContext.add_cases (RuleCases.make true goal [rule_contextN]))
+    |> map_context (ProofContext.add_cases
+     (if length props = 1 then RuleCases.make true goal [rule_contextN]
+      else [(rule_contextN, RuleCases.empty)]))
     |> auto_bind_goal props
     |> (if is_chain state then use_facts else reset_facts)
     |> new_block