# HG changeset patch
# User wenzelm
# Date 1635092961 -7200
# Node ID f4613ca298e6aba075c58614da12bebcf91ae346
# Parent  7f311d474cf945c75b91124a757a034017dc5a29
more antiquotations;

diff -r 7f311d474cf9 -r f4613ca298e6 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Oct 24 18:02:58 2021 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Oct 24 18:29:21 2021 +0200
@@ -659,8 +659,9 @@
 
 local
 
-fun pol (ctxt, ct, t) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: pol \<Rightarrow> pol \<Rightarrow> prop\<close>
-  ct (Thm.cterm_of ctxt t);
+fun pol (ctxt, ct, t) =
+  \<^let>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
+    in cterm \<open>x \<equiv> y\<close> for x y :: pol\<close>;
 
 val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (\<^binding>\<open>pnsubstl\<close>, pol)));
diff -r 7f311d474cf9 -r f4613ca298e6 src/HOL/Decision_Procs/Reflective_Field.thy
--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Sun Oct 24 18:02:58 2021 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Sun Oct 24 18:29:21 2021 +0200
@@ -639,8 +639,9 @@
 
 local
 
-fun fnorm (ctxt, ct, t) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: pexpr \<times> pexpr \<times> pexpr list \<Rightarrow> pexpr \<times> pexpr \<times> pexpr list \<Rightarrow> prop\<close>
-  ct (Thm.cterm_of ctxt t);
+fun fnorm (ctxt, ct, t) =
+  \<^let>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
+    in cterm \<open>x \<equiv> y\<close> for x y :: \<open>pexpr \<times> pexpr \<times> pexpr list\<close>\<close>;
 
 val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (\<^binding>\<open>fnorm\<close>, fnorm)));
@@ -880,8 +881,7 @@
       val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
       val ce = Thm.cterm_of ctxt (reif xs t);
       val ce' = Thm.cterm_of ctxt (reif xs u);
-      val fnorm = cv ctxt
-        (Thm.apply \<^cterm>\<open>fnorm\<close> (Thm.apply (Thm.apply \<^cterm>\<open>FSub\<close> ce) ce'));
+      val fnorm = cv ctxt \<^let>\<open>e = ce and e' = ce' in cterm \<open>fnorm (FSub e e')\<close>\<close>;
       val (_, [n, dc]) = strip_app (Thm.rhs_of fnorm);
       val (_, [_, c]) = strip_app dc;
       val th =
diff -r 7f311d474cf9 -r f4613ca298e6 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sun Oct 24 18:02:58 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Sun Oct 24 18:29:21 2021 +0200
@@ -81,7 +81,7 @@
   | _ => [ct]);
 
 val list_conj =
-  foldr1 (fn (c, c') => Thm.apply (Thm.apply \<^cterm>\<open>HOL.conj\<close> c) c');
+  foldr1 (fn (A, B) => \<^let>\<open>A = A and B = B in cterm \<open>A \<and> B\<close>\<close>);
 
 fun mk_conj_tab th =
   let
@@ -133,7 +133,6 @@
         val e = Thm.dest_fun ct
         val (x,p) = Thm.dest_abs_global (Thm.dest_arg ct)
         val Free (xn, _) = Thm.term_of x
-        val Pp = Thm.apply \<^cterm>\<open>Trueprop\<close> p
         val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
       in
         (case eqs of
@@ -144,8 +143,8 @@
               case ndx of
                 [] => NONE
               | _ =>
-                conj_aci_rule (Thm.mk_binop \<^cterm>\<open>(\<equiv>) :: prop => _\<close> Pp
-                  (Thm.apply \<^cterm>\<open>Trueprop\<close> (list_conj (ndx @ dx))))
+                conj_aci_rule
+                  \<^let>\<open>A = p and B = \<open>list_conj (ndx @ dx)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
                 |> Thm.abstract_rule xn x
                 |> Drule.arg_cong_rule e
                 |> Conv.fconv_rule
@@ -155,8 +154,8 @@
                 |> SOME
             end
         | _ =>
-            conj_aci_rule (Thm.mk_binop \<^cterm>\<open>(\<equiv>) :: prop => _\<close> Pp
-              (Thm.apply \<^cterm>\<open>Trueprop\<close> (list_conj (eqs @ neqs))))
+            conj_aci_rule
+              \<^let>\<open>A = p and B = \<open>list_conj (eqs @ neqs)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
             |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
             |> Conv.fconv_rule
                 (Conv.arg_conv