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;