diff -r b4d409c65a76 -r 71467e35fc3c src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Tue Nov 26 14:32:08 2019 +0000
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Nov 28 18:13:23 2019 +0100
@@ -314,6 +314,7 @@
       SOME (transform_function_data (inst_morph u) data) handle Pattern.MATCH => NONE
   in
     get_first match (retrieve_function_data ctxt t)
+    |> Option.map (transform_function_data (Morphism.transfer_morphism' ctxt))
   end
 
 fun import_last_function ctxt =