--- 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'
--- a/src/HOL/Tools/Quotient/quotient_type.ML Sat Aug 10 20:46:12 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Sat Aug 10 21:13:37 2024 +0200
@@ -314,7 +314,7 @@
val tmp_lthy1 = Variable.declare_typ rty lthy
val rel =
Syntax.parse_term tmp_lthy1 rel_str
- |> Type.constraint (rty --> rty --> \<^typ>\<open>bool\<close>)
+ |> Type.constraint \<^Type>\<open>fun rty \<^Type>\<open>fun rty \<^Type>\<open>bool\<close>\<close>\<close>
|> Syntax.check_term tmp_lthy1
val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm