# HG changeset patch
# User wenzelm
# Date 1635587963 -7200
# Node ID 994a2b9daf1dcc4caa667f60a6c8e37841f9855f
# Parent  8ab92e40dde6d55957049bac0615d97709d257c4
clarified antiquotations;

diff -r 8ab92e40dde6 -r 994a2b9daf1d src/HOL/Library/Cancellation/cancel_data.ML
--- a/src/HOL/Library/Cancellation/cancel_data.ML	Fri Oct 29 21:06:08 2021 +0200
+++ b/src/HOL/Library/Cancellation/cancel_data.ML	Sat Oct 30 11:59:23 2021 +0200
@@ -30,10 +30,7 @@
 
 (*No reordering of the arguments.*)
 fun fast_mk_iterate_add (n, mset) =
-  let val T = fastype_of mset
-  in
-    Const (\<^const_name>\<open>iterate_add\<close>, \<^typ>\<open>nat\<close> --> T --> T) $ n $ mset
-  end;
+  \<^Const>\<open>iterate_add \<open>fastype_of mset\<close> for n mset\<close>;
 
 (*iterate_add is not symmetric, unlike multiplication over natural numbers.*)
 fun mk_iterate_add (t, u) =
@@ -56,16 +53,16 @@
     handle TERM _ => find_first_numeral (t::past) terms)
   | find_first_numeral _ [] = raise TERM("find_first_numeral", []);
 
-fun typed_zero T = Const (\<^const_name>\<open>Groups.zero\<close>, T);
-fun typed_one T = HOLogic.numeral_const T $ HOLogic.one_const
-val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Groups.plus\<close>;
+fun typed_zero T = \<^Const>\<open>Groups.zero T\<close>;
+fun typed_one T = \<^Const>\<open>numeral T for \<^Const>\<open>num.One\<close>\<close>;
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>plus\<close>;
 
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero.*)
 fun mk_sum T [] = typed_zero T
   | mk_sum _ [t,u] = mk_plus (t, u)
   | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
 
-val dest_plus = HOLogic.dest_bin \<^const_name>\<open>Groups.plus\<close> dummyT;
+val dest_plus = HOLogic.dest_bin \<^const_name>\<open>plus\<close> dummyT;
 
 
 (*** Other simproc items ***)
diff -r 8ab92e40dde6 -r 994a2b9daf1d src/HOL/Library/Cancellation/cancel_simprocs.ML
--- a/src/HOL/Library/Cancellation/cancel_simprocs.ML	Fri Oct 29 21:06:08 2021 +0200
+++ b/src/HOL/Library/Cancellation/cancel_simprocs.ML	Sat Oct 30 11:59:23 2021 +0200
@@ -26,24 +26,24 @@
 
 structure Eq_Cancel_Comm_Monoid_less = Cancel_Fun
  (open Cancel_Data
-  val mk_bal   = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less\<close>
-  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less\<close> dummyT
+  val mk_bal   = HOLogic.mk_binrel \<^const_name>\<open>less\<close>
+  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>less\<close> dummyT
   val bal_add1 = @{thm iterate_add_less_iff1} RS trans
   val bal_add2 = @{thm iterate_add_less_iff2} RS trans
 );
 
 structure Eq_Cancel_Comm_Monoid_less_eq = Cancel_Fun
  (open Cancel_Data
-  val mk_bal   = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less_eq\<close>
-  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less_eq\<close> dummyT
+  val mk_bal   = HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
+  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>less_eq\<close> dummyT
   val bal_add1 = @{thm iterate_add_less_eq_iff1} RS trans
   val bal_add2 = @{thm iterate_add_less_eq_iff2} RS trans
 );
 
 structure Diff_Cancel_Comm_Monoid_less_eq = Cancel_Fun
  (open Cancel_Data
-  val mk_bal   = HOLogic.mk_binop \<^const_name>\<open>Groups.minus\<close>
-  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Groups.minus\<close> dummyT
+  val mk_bal   = HOLogic.mk_binop \<^const_name>\<open>minus\<close>
+  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>minus\<close> dummyT
   val bal_add1 = @{thm iterate_add_add_eq1} RS trans
   val bal_add2 = @{thm iterate_add_diff_add_eq2} RS trans
 );