diff -r 9179e7a98196 -r 235396695401 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Tue Aug 06 17:26:40 2019 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Tue Aug 06 19:07:12 2019 +0200
@@ -96,8 +96,9 @@
     val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i NONE state
     val tn = find_tname ctxt' var (map Thm.term_of asms)
     val rule =
-        if exh then #exhaustion (datatype_info thy tn)
-               else #induct  (datatype_info thy tn)
+      datatype_info thy tn
+      |> (if exh then #exhaustion else #induct)
+      |> Thm.transfer thy;
     val (Const(\<^const_name>\<open>mem\<close>,_) $ Var(ixn,_) $ _) =
         (case Thm.prems_of rule of
              [] => error "induction is not available for this datatype"
@@ -136,11 +137,11 @@
     val dt_info =
           {inductive = true,
            constructors = constructors,
-           rec_rewrites = recursor_eqns,
-           case_rewrites = case_eqns,
-           induct = induct,
-           mutual_induct = @{thm TrueI},  (*No need for mutual induction*)
-           exhaustion = elim};
+           rec_rewrites = map Thm.trim_context recursor_eqns,
+           case_rewrites = map Thm.trim_context case_eqns,
+           induct = Thm.trim_context induct,
+           mutual_induct = Thm.trim_context @{thm TrueI},  (*No need for mutual induction*)
+           exhaustion = Thm.trim_context elim};
 
     val con_info =
           {big_rec_name = big_rec_name,
@@ -149,8 +150,9 @@
            free_iffs = [],  (*thus we expect the necessary freeness rewrites
                               to be in the simpset already, as is the case for
                               Nat and disjoint sum*)
-           rec_rewrites = (case recursor_eqns of
-                               [] => case_eqns | _ => recursor_eqns)};
+           rec_rewrites =
+            (case recursor_eqns of [] => case_eqns | _ => recursor_eqns)
+            |> map Thm.trim_context};
 
     (*associate with each constructor the datatype name and rewrites*)
     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors