src/HOL/Tools/lin_arith.ML

--- a/src/HOL/Tools/lin_arith.ML	Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sun Feb 18 15:05:21 2018 +0100
@@ -87,7 +87,7 @@
 
 fun get_splits ctxt =
   #splits (get_arith_data ctxt)
-  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+  |> map (Thm.transfer' ctxt);
 
 fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
   {splits = update Thm.eq_thm_prop (Thm.trim_context thm) splits,