# 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 =