--- 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)