# HG changeset patch
# User traytel
# Date 1584276093 -3600
# Node ID 1cf958713cf7c317cda992d4371f17febe19c314
# Parent  61ba52af28e340ee1bf67a77b2501ad84966cae3
remove Thm.transfer workaround made obsplete by cf2406e654cf

diff -r 61ba52af28e3 -r 1cf958713cf7 src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Sun Mar 15 13:20:22 2020 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Sun Mar 15 13:41:33 2020 +0100
@@ -2012,14 +2012,10 @@
               else bad_input [thm])
       | NONE => (case Lifting_Info.lookup_quotients lthy absT_name of
             SOME {quot_thm = qthm, ...} =>
-              let
-                val qthm = Thm.transfer' lthy qthm;
-              in
-                case [qthm] RL @{thms Quotient_eq_onp_typedef Quotient_eq_onp_type_copy} of
-                  thm :: _ => (thm, Typedef)
-                | _ => (qthm RS @{thm Quotient_Quotient3},
-                   Quotient (find_equiv_thm_via_Quotient qthm))
-              end
+              (case [qthm] RL @{thms Quotient_eq_onp_typedef Quotient_eq_onp_type_copy} of
+                thm :: _ => (thm, Typedef)
+              | _ => (qthm RS @{thm Quotient_Quotient3},
+                 Quotient (find_equiv_thm_via_Quotient qthm)))
           | NONE => (Typedef.get_info lthy absT_name |> hd |> snd |> #type_definition, Typedef))
       | SOME thms => bad_input thms);
     val wits = (Option.map o map) (prepare_term lthy) raw_wits;