src/HOL/Tools/Transfer/transfer.ML
changeset 67664 ad2b3e330c27
parent 67399 eab6ce8368fa
child 69593 3dda49e08b9d
--- a/src/HOL/Tools/Transfer/transfer.ML	Mon Feb 19 14:30:06 2018 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML	Mon Feb 19 14:49:11 2018 +0100
@@ -868,7 +868,7 @@
   end
 
 fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
-  |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+  |> Option.map (morph_pred_data (Morphism.transfer_morphism' ctxt))
 
 fun update_pred_data type_name qinfo ctxt =
   Data.map (map_pred_data (Symtab.update (type_name, qinfo))) ctxt