--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Aug 08 16:21:48 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Aug 08 16:23:30 2024 +0200
@@ -607,8 +607,8 @@
| (_, Const _) =>
let
val thy = Proof_Context.theory_of ctxt
- fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T'
- | same_const _ _ = false
+ fun same_const t u =
+ eq_Const_name (t, u) andalso matches_typ ctxt (dest_Const_type t) (dest_Const_type u)
in
if same_const rtrm qtrm then rtrm
else