RuleCases.make true;

--- a/src/Pure/Isar/proof.ML	Mon Nov 06 22:52:35 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 06 22:53:00 2000 +0100
@@ -591,7 +591,7 @@
   in
     state'
     |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds))
-    |> map_context (ProofContext.add_cases (RuleCases.make false goal [antN]))
+    |> map_context (ProofContext.add_cases (RuleCases.make true goal [antN]))
     |> auto_bind_goal prop
     |> (if is_chain state then use_facts else reset_facts)
     |> new_block