# HG changeset patch
# User wenzelm
# Date 973547580 -3600
# Node ID 1820abac64fea11673154a124d12e80115f99e2a
# Parent  9a23abbc81facc5b042257c691ea509058dae483
RuleCases.make true;

diff -r 9a23abbc81fa -r 1820abac64fe src/Pure/Isar/proof.ML
--- 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