[mq]: noworkaround draft
authortraytel
Sun, 15 Mar 2020 11:32:56 +0100
changeset 71768 bb923365f9da
parent 71767 cf2406e654cf
[mq]: noworkaround
src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Sat Mar 14 21:58:29 2020 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Sun Mar 15 11:32:56 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;