# HG changeset patch
# User wenzelm
# Date 1723987758 -7200
# Node ID b7d051e25d9dab681984e5f7de4c92d4e90b3154
# Parent  ac39d932ddfc6bbddedaa80e97dbc4b8ced8d529
tuned: more antiquotations;

diff -r ac39d932ddfc -r b7d051e25d9d src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Sun Aug 18 15:29:03 2024 +0200
+++ b/src/HOL/Tools/arith_data.ML	Sun Aug 18 15:29:18 2024 +0200
@@ -57,29 +57,21 @@
 fun mk_number T 1 = HOLogic.numeral_const T $ HOLogic.one_const
   | mk_number T n = HOLogic.mk_number T n;
 
-val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Groups.plus\<close>;
-
-fun mk_minus t =
-  let val T = Term.fastype_of t
-  in Const (\<^const_name>\<open>Groups.uminus\<close>, T --> T) $ t end;
-
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
 fun mk_sum T [] = mk_number T 0
-  | mk_sum T [t, u] = mk_plus (t, u)
-  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
+  | mk_sum T [t, u] = \<^Const>\<open>plus T for t u\<close>
+  | mk_sum T (t :: ts) = \<^Const>\<open>plus T for t \<open>mk_sum T ts\<close>\<close>;
 
 (*this version ALWAYS includes a trailing zero*)
 fun long_mk_sum T [] = mk_number T 0
-  | long_mk_sum T (t :: ts) = mk_plus (t, long_mk_sum T ts);
+  | long_mk_sum T (t :: ts) = \<^Const>\<open>plus T for t \<open>long_mk_sum T ts\<close>\<close>;
 
 (*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const (\<^const_name>\<open>Groups.plus\<close>, _) $ t $ u, ts) =
-      dest_summing (pos, t, dest_summing (pos, u, ts))
-  | dest_summing (pos, Const (\<^const_name>\<open>Groups.minus\<close>, _) $ t $ u, ts) =
-      dest_summing (pos, t, dest_summing (not pos, u, ts))
-  | dest_summing (pos, t, ts) = (if pos then t else mk_minus t) :: ts;
+fun dest_summing pos \<^Const_>\<open>plus _ for t u\<close> ts = dest_summing pos t (dest_summing pos u ts)
+  | dest_summing pos \<^Const_>\<open>minus _ for t u\<close> ts = dest_summing pos t (dest_summing (not pos) u ts)
+  | dest_summing pos t ts = (if pos then t else \<^Const>\<open>uminus \<open>fastype_of t\<close> for t\<close>) :: ts;
 
-fun dest_sum t = dest_summing (true, t, []);
+fun dest_sum t = dest_summing true t [];
 
 
 (* various auxiliary and legacy *)
diff -r ac39d932ddfc -r b7d051e25d9d src/HOL/Tools/boolean_algebra_cancel.ML
--- a/src/HOL/Tools/boolean_algebra_cancel.ML	Sun Aug 18 15:29:03 2024 +0200
+++ b/src/HOL/Tools/boolean_algebra_cancel.ML	Sun Aug 18 15:29:18 2024 +0200
@@ -16,19 +16,19 @@
 
 fun move_to_front rule path = Conv.rewr_conv (Library.foldl (op RS) (rule, path))
 
-fun add_atoms sup pos path (t as Const (\<^const_name>\<open>Lattices.sup\<close>, _) $ x $ y) =
+fun add_atoms sup pos path (t as \<^Const_>\<open>sup _ for x y\<close>) =
     if sup then
       add_atoms sup pos (@{thm boolean_algebra_cancel.sup1}::path) x #>
       add_atoms sup pos (@{thm boolean_algebra_cancel.sup2}::path) y
     else cons ((pos, t), path)
-  | add_atoms sup pos path (t as Const (\<^const_name>\<open>Lattices.inf\<close>, _) $ x $ y) =
+  | add_atoms sup pos path (t as \<^Const_>\<open>inf _ for x y\<close>) =
     if not sup then
       add_atoms sup pos (@{thm boolean_algebra_cancel.inf1}::path) x #>
       add_atoms sup pos (@{thm boolean_algebra_cancel.inf2}::path) y
     else cons ((pos, t), path)
-  | add_atoms _ _ _ (Const (\<^const_name>\<open>Orderings.bot\<close>, _)) = I
-  | add_atoms _ _ _ (Const (\<^const_name>\<open>Orderings.top\<close>, _)) = I
-  | add_atoms _ pos path (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ x) = cons ((not pos, x), path)
+  | add_atoms _ _ _ \<^Const_>\<open>bot _\<close> = I
+  | add_atoms _ _ _ \<^Const_>\<open>top _\<close> = I
+  | add_atoms _ pos path \<^Const_>\<open>uminus _ for x\<close> = cons ((not pos, x), path)
   | add_atoms _ pos path x = cons ((pos, x), path);
 
 fun atoms sup pos t = add_atoms sup pos [] t []
diff -r ac39d932ddfc -r b7d051e25d9d src/HOL/Tools/group_cancel.ML
--- a/src/HOL/Tools/group_cancel.ML	Sun Aug 18 15:29:03 2024 +0200
+++ b/src/HOL/Tools/group_cancel.ML	Sun Aug 18 15:29:18 2024 +0200
@@ -24,15 +24,15 @@
     [Conv.rewr_conv (Library.foldl (op RS) (@{thm group_cancel.rule0}, path)),
      Conv.arg1_conv (Conv.repeat_conv (Conv.rewr_conv minus_minus))]
 
-fun add_atoms pos path (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ x $ y) =
+fun add_atoms pos path \<^Const_>\<open>plus _ for x y\<close> =
       add_atoms pos (@{thm group_cancel.add1}::path) x #>
       add_atoms pos (@{thm group_cancel.add2}::path) y
-  | add_atoms pos path (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ x $ y) =
+  | add_atoms pos path \<^Const_>\<open>minus _ for x y\<close> =
       add_atoms pos (@{thm group_cancel.sub1}::path) x #>
       add_atoms (not pos) (@{thm group_cancel.sub2}::path) y
-  | add_atoms pos path (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ x) =
+  | add_atoms pos path \<^Const_>\<open>uminus _ for x\<close> =
       add_atoms (not pos) (@{thm group_cancel.neg1}::path) x
-  | add_atoms _ _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I
+  | add_atoms _ _ \<^Const_>\<open>Groups.zero _\<close> = I
   | add_atoms pos path x = cons ((pos, x), path)
 
 fun atoms t = add_atoms true [] t []
diff -r ac39d932ddfc -r b7d051e25d9d src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Sun Aug 18 15:29:03 2024 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Sun Aug 18 15:29:18 2024 +0200
@@ -21,12 +21,12 @@
     [Conv.rewr_conv (Library.foldl (op RS) (@{thm nat_arith.rule0}, path)),
      Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
 
-fun add_atoms path (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ x $ y) =
+fun add_atoms path \<^Const_>\<open>plus _ for x y\<close> =
       add_atoms (@{thm nat_arith.add1}::path) x #>
       add_atoms (@{thm nat_arith.add2}::path) y
-  | add_atoms path (Const (\<^const_name>\<open>Nat.Suc\<close>, _) $ x) =
+  | add_atoms path \<^Const_>\<open>Suc for x\<close> =
       add_atoms (@{thm nat_arith.suc1}::path) x
-  | add_atoms _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I
+  | add_atoms _ \<^Const_>\<open>Groups.zero _\<close> = I
   | add_atoms path x = cons (x, path)
 
 fun atoms t = add_atoms [] t []