src/HOL/Tools/inductive.ML

 
 (* monotonicity rules *)
 
 fun get_monos ctxt =
   #monos (rep_data ctxt)
-  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+  |> map (Thm.transfer' ctxt);
 
 fun mk_mono ctxt thm =
   let
     fun eq_to_mono thm' = thm' RS (thm' RS @{thm eq_to_mono});
     fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})

 
 (* equations *)
 
 fun retrieve_equations ctxt =
   Item_Net.retrieve (#equations (rep_data ctxt))
-  #> map (Thm.transfer (Proof_Context.theory_of ctxt));
+  #> map (Thm.transfer' ctxt);
 
 val equation_add_permissive =
   Thm.declaration_attribute (fn thm =>
     map_data (fn (infos, monos, equations) =>
       (infos, monos, perhaps (try (Item_Net.update (Thm.trim_context thm))) equations)));