# HG changeset patch
# User wenzelm
# Date 1723317217 -7200
# Node ID 9b29c5d7aae43df993fef9422b5e975809c64637
# Parent  dfafe46a37c4bea01bdbaf95e6c5c8bebe539be5
tuned: more antiquotations;

diff -r dfafe46a37c4 -r 9b29c5d7aae4 src/HOL/Tools/Quotient/quotient_term.ML
--- 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'
diff -r dfafe46a37c4 -r 9b29c5d7aae4 src/HOL/Tools/Quotient/quotient_type.ML
--- 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