diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -156,7 +156,7 @@
     val concl_pat = Drule.strip_imp_concl (Thm.cprop_of rule)
     val insts = Thm.first_order_match (concl_pat, cprop)
     val rule = Drule.instantiate_normalize insts rule
-    val prop = hd (Thm.prems_of rule)
+    val prop = hd (Thm.take_prems_of 1 rule)
   in
     case mono_eq_prover ctxt prop of
       SOME thm => SOME (thm RS rule)
@@ -233,7 +233,7 @@
     val preprocessed_thm = preprocess ctxt0 thm
     val (fixed_thm, ctxt1) = ctxt0
       |> yield_singleton (apfst snd oo Variable.import true) preprocessed_thm
-    val assms = cprems_of fixed_thm
+    val assms = Thm.cprems_of fixed_thm
     val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add
     val (prems, ctxt2) = ctxt1 |> fold_map Thm.assume_hyps assms
     val ctxt3 =  ctxt2 |> Context.proof_map (fold add_transfer_rule prems)
@@ -386,7 +386,7 @@
         val rel_fun = prove_rel ctxt rsp_thm (rty, qty)
         val rep_abs_thm = [quot_thm, rel_fun] MRSL @{thm Quotient_rep_abs_eq}
       in
-        case mono_eq_prover ctxt (hd (Thm.prems_of rep_abs_thm)) of
+        case mono_eq_prover ctxt (hd (Thm.take_prems_of 1 rep_abs_thm)) of
           SOME mono_eq_thm =>
             let
               val rep_abs_eq = mono_eq_thm RS rep_abs_thm