--- 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;