changeset 70318 | 9eff9e2dc177 |
parent 70308 | 7f568724d67e |
--- a/src/HOL/Tools/Function/fun_cases.ML Tue Jun 04 13:44:59 2019 +0200 +++ b/src/HOL/Tools/Function/fun_cases.ML Tue Jun 04 15:11:29 2019 +0200 @@ -33,7 +33,7 @@ fun mk_elim rl = Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl)) - |> singleton (Variable.export (Proof_Context.augment prop ctxt) ctxt); + |> singleton (Proof_Context.export (Proof_Context.augment prop ctxt) ctxt); in (case get_first (try mk_elim) (flat elims) of SOME r => r