--- a/src/HOL/Tools/inductive.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Tools/inductive.ML Sun Feb 18 15:05:21 2018 +0100
@@ -276,7 +276,7 @@
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
@@ -314,7 +314,7 @@
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 =>