diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Sep 27 16:44:50 2002 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Sep 30 15:44:21 2002 +0200
@@ -685,7 +685,7 @@
       (after_qed o map_context gen_binds, pr)))
     |> map_context (ProofContext.add_cases
      (if length props = 1 then
-      RuleCases.make true None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
+      RuleCases.make None None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
       else [(rule_contextN, RuleCases.empty)]))
     |> auto_bind_goal props
     |> (if is_chain state then use_facts else reset_facts)