equal
deleted
inserted
replaced
31 val elims = if is_partial then pelims else the elims; |
31 val elims = if is_partial then pelims else the elims; |
32 val cprop = Thm.cterm_of ctxt prop; |
32 val cprop = Thm.cterm_of ctxt prop; |
33 fun mk_elim rl = |
33 fun mk_elim rl = |
34 Thm.implies_intr cprop |
34 Thm.implies_intr cprop |
35 (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl)) |
35 (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl)) |
36 |> singleton (Variable.export (Proof_Context.augment prop ctxt) ctxt); |
36 |> singleton (Proof_Context.export (Proof_Context.augment prop ctxt) ctxt); |
37 in |
37 in |
38 (case get_first (try mk_elim) (flat elims) of |
38 (case get_first (try mk_elim) (flat elims) of |
39 SOME r => r |
39 SOME r => r |
40 | NONE => err ()) |
40 | NONE => err ()) |
41 end; |
41 end; |