--- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Jan 21 23:28:34 2025 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Jan 22 19:34:04 2025 +0100
@@ -417,7 +417,7 @@
val ctm = Thm.dest_equals_lhs (Thm.cprop_of rep_id)
val unfolded_maps_eq = unfold_fun_maps ctm
val t1 = [quot_thm, def_thm, rsp_thm] MRSL @{thm Quotient_rep_abs_fold_unmap}
- val prems_pat = (hd o Drule.cprems_of) t1
+ val prems_pat = Thm.cprem_of t1 1
val insts = Thm.first_order_match (prems_pat, Thm.cprop_of unfolded_maps_eq)
in
unfolded_maps_eq RS (Drule.instantiate_normalize insts t1)