more antiquotations;

--- a/src/ZF/arith_data.ML	Sat Sep 11 22:28:01 2021 +0200
+++ b/src/ZF/arith_data.ML	Sat Sep 11 22:38:41 2021 +0200
@@ -29,7 +29,7 @@
 fun mk_succ t = succ $ t;
 val one = mk_succ zero;
 
-val mk_plus = FOLogic.mk_binop \<^const_name>\<open>Arith.add\<close>;
+fun mk_plus (t, u) = \<^Const>\<open>Arith.add for t u\<close>;
 
 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
@@ -80,7 +80,7 @@
 (*** Use CancelNumerals simproc without binary numerals,
      just for cancellation ***)
 
-val mk_times = FOLogic.mk_binop \<^const_name>\<open>Arith.mult\<close>;
+fun mk_times (t, u) = \<^Const>\<open>Arith.mult for t u\<close>;
 
 fun mk_prod [] = one
   | mk_prod [t] = t
@@ -175,7 +175,7 @@
   struct
   open CancelNumeralsCommon
   val prove_conv = prove_conv "natless_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binrel \<^const_name>\<open>Ordinal.lt\<close>
+  fun mk_bal (t, u) = \<^Const>\<open>Ordinal.lt for t u\<close>
   val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Ordinal.lt\<close> iT
   val bal_add1 = @{thm less_add_iff [THEN iff_trans]}
   val bal_add2 = @{thm less_add_iff [THEN iff_trans]}
@@ -188,7 +188,7 @@
   struct
   open CancelNumeralsCommon
   val prove_conv = prove_conv "natdiff_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binop \<^const_name>\<open>Arith.diff\<close>
+  fun mk_bal (t, u) = \<^Const>\<open>Arith.diff for t u\<close>
   val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Arith.diff\<close> iT
   val bal_add1 = @{thm diff_add_eq [THEN trans]}
   val bal_add2 = @{thm diff_add_eq [THEN trans]}

--- a/src/ZF/int_arith.ML	Sat Sep 11 22:28:01 2021 +0200
+++ b/src/ZF/int_arith.ML	Sat Sep 11 22:38:41 2021 +0200
@@ -53,7 +53,7 @@
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
 val zero = mk_numeral 0;
-val mk_plus = FOLogic.mk_binop \<^const_name>\<open>zadd\<close>;
+fun mk_plus (t, u) = \<^Const>\<open>zadd for t u\<close>;
 
 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
@@ -75,7 +75,7 @@
 fun dest_sum t = dest_summing (true, t, []);
 
 val one = mk_numeral 1;
-val mk_times = FOLogic.mk_binop \<^const_name>\<open>zmult\<close>;
+fun mk_times (t, u) = \<^Const>\<open>zmult for t u\<close>;
 
 fun mk_prod [] = one
   | mk_prod [t] = t
@@ -191,7 +191,7 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binrel \<^const_name>\<open>zless\<close>
+  fun mk_bal (t, u) = \<^Const>\<open>zless for t u\<close>
   val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zless\<close> \<^typ>\<open>i\<close>
   val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans}
   val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans}
@@ -200,7 +200,7 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binrel \<^const_name>\<open>zle\<close>
+  fun mk_bal (t, u) = \<^Const>\<open>zle for t u\<close>
   val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zle\<close> \<^typ>\<open>i\<close>
   val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans}
   val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans}