diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -12,6 +12,7 @@
     Attrib.binding * term -> local_theory -> (term * thm) * local_theory
   val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->
     Attrib.binding * string -> local_theory -> (term * thm) * local_theory
+  val transform_result: morphism -> term * thm -> term * thm
 end;
 
 structure Partial_Function: PARTIAL_FUNCTION =
@@ -219,6 +220,8 @@
 
 (*** partial_function definition ***)
 
+fun transform_result phi (t, thm) = (Morphism.term phi t, Morphism.thm phi thm);
+
 fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
   let
     val setup_data = the (lookup_mode lthy mode)