--- 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)