src/Pure/Isar/proof.ML

     |> map_context (autofix props)
     |> put_goal (Some (((kind, names, propss), ([], goal)),
       (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)
     |> new_block
     |> enter_backward