src/Pure/Isar/proof.ML

     fun subgoals 0 = ""
       | subgoals 1 = ", 1 subgoal"
       | 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
         (if mode <> Backward orelse null goal_facts then None else Some goal_facts) @
       [Pretty.str ("goal (" ^ kind_name (sign_of state) kind ^ prt_names names ^

     else warning ("Goal statement contains unbound schematic variable(s): " ^
       commas (map (ProofContext.string_of_term (context_of state')) vars));
     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
     |> enter_backward
   end;