diff -r cbfc1058df7c -r 28e8d402a9ba src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Wed Aug 07 20:56:31 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Thu Aug 08 14:24:18 2024 +0200
@@ -7,6 +7,7 @@
 signature LIFTING_UTIL =
 sig
   val MRSL: thm list * thm -> thm
+  val mk_Quotient: term * term * term * term -> term
   val dest_Quotient: term -> term * term * term * term
 
   val quot_thm_rel: thm -> term
@@ -40,8 +41,11 @@
 
 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
 
-fun dest_Quotient (Const (\<^const_name>\<open>Quotient\<close>, _) $ rel $ abs $ rep $ cr)
-      = (rel, abs, rep, cr)
+fun mk_Quotient (rel, abs, rep, cr) =
+  let val \<^Type>\<open>fun A B\<close> = fastype_of abs
+  in \<^Const>\<open>Quotient A B for rel abs rep cr\<close> end
+
+fun dest_Quotient \<^Const_>\<open>Quotient _ _ for rel abs rep cr\<close> = (rel, abs, rep, cr)
   | dest_Quotient t = raise TERM ("dest_Quotient", [t])
 
 (*