--- a/src/HOL/Tools/Quotient/quotient_term.ML Sat Aug 10 20:46:12 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Sat Aug 10 21:13:37 2024 +0200
@@ -310,7 +310,7 @@
val rtys' = map (Envir.subst_type qtyenv) rtys
val args = map (equiv_relation ctxt) (tys ~~ rtys')
val eqv_rel = get_equiv_rel ctxt s'
- val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> \<^typ>\<open>bool\<close>)
+ val eqv_rel' = force_typ ctxt eqv_rel \<^Type>\<open>fun rty \<^Type>\<open>fun rty \<^Type>\<open>bool\<close>\<close>\<close>
in
if forall is_eq args
then eqv_rel'