src/HOL/Tools/Function/function_context_tree.ML
changeset 67649 1e1782c1aedf
parent 65418 c821f1f3d92d
child 67710 cc2db3239932
--- a/src/HOL/Tools/Function/function_context_tree.ML	Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Tools/Function/function_context_tree.ML	Sun Feb 18 15:05:21 2018 +0100
@@ -53,7 +53,7 @@
 
 fun get_function_congs ctxt =
   FunctionCongs.get (Context.Proof ctxt)
-  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+  |> map (Thm.transfer' ctxt);
 
 val add_function_cong = FunctionCongs.map o Thm.add_thm o Thm.trim_context;