# HG changeset patch # User wenzelm # Date 1683835963 -7200 # Node ID 2594319ad9eec33e6736cf87e7383364302a4ebb # Parent bd5f6cee8001e5b0fb9f80ee6a8b7503700e6d6b proper Thm.trim_context / Thm.transfer; diff -r bd5f6cee8001 -r 2594319ad9ee src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu May 11 21:32:22 2023 +0200 +++ b/src/ZF/Tools/inductive_package.ML Thu May 11 22:12:43 2023 +0200 @@ -274,6 +274,7 @@ |> Global_Theory.add_thm ((Binding.name "elim", rule_by_tactic ctxt3 (basic_elim_tac ctxt3) (unfold RS Ind_Syntax.equals_CollectD)), []); + val elim' = Thm.trim_context elim; val ctxt4 = Proof_Context.init_global thy4; @@ -284,7 +285,7 @@ fun make_cases ctxt A = rule_by_tactic ctxt (basic_elim_tac ctxt THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac ctxt) - (Thm.assume A RS elim) + (Thm.assume A RS Thm.transfer' ctxt elim') |> Drule.export_without_context_open; fun induction_rules raw_induct =