changeset 70473 | 9179e7a98196 |
parent 70320 | 59258a3192bf |
child 70494 | 41108e3e9ca5 |
--- 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