diff -r cf66d2db97fe -r 9179e7a98196 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Aug 06 16:29:28 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Aug 06 17:26:40 2019 +0200
@@ -624,7 +624,7 @@
   let
     fun collect (data : Lifting_Info.quotient) l =
       if is_some (#pcr_info data)
-      then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l)
+      then ((Thm.symmetric o safe_mk_meta_eq o Thm.transfer' ctxt o #pcr_cr_eq o the o #pcr_info) data :: l)
       else l
     val table = Lifting_Info.get_quotients ctxt
   in