# HG changeset patch
# User wenzelm
# Date 1723984849 -7200
# Node ID 41cdf0fb32fa4c6fa516622d29c6324ad10df952
# Parent  f3c9203d82c3e5cf3e78c7416fb416fa25faba9f
tuned: more antiquotations;

diff -r f3c9203d82c3 -r 41cdf0fb32fa src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sun Aug 18 14:22:21 2024 +0200
+++ b/src/HOL/Tools/groebner.ML	Sun Aug 18 14:40:49 2024 +0200
@@ -349,23 +349,23 @@
 
 fun refute_disj rfn tm =
  case Thm.term_of tm of
-  Const(\<^const_name>\<open>HOL.disj\<close>,_)$_$_ =>
+  \<^Const_>\<open>disj for _ _\<close> =>
    Drule.compose
     (refute_disj rfn (Thm.dest_arg tm), 2,
       Drule.compose (refute_disj rfn (Thm.dest_arg1 tm), 2, disjE))
   | _ => rfn tm ;
 
-val notnotD = @{thm notnotD};
 fun mk_binop ct x y = Thm.apply (Thm.apply ct x) y
 
 fun is_neg t =
-    case Thm.term_of t of
-      (Const(\<^const_name>\<open>Not\<close>,_)$_) => true
-    | _  => false;
+  case Thm.term_of t of
+    \<^Const_>\<open>Not for _\<close> => true
+  | _  => false;
+
 fun is_eq t =
- case Thm.term_of t of
- (Const(\<^const_name>\<open>HOL.eq\<close>,_)$_$_) => true
-| _  => false;
+  case Thm.term_of t of
+    \<^Const_>\<open>HOL.eq _ for _ _\<close> => true
+  | _  => false;
 
 fun end_itlist f l =
   case l of
@@ -392,9 +392,9 @@
  end;
 
 fun is_forall t =
- case Thm.term_of t of
-  (Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,_)) => true
-| _ => false;
+  case Thm.term_of t of
+    \<^Const_>\<open>All _ for \<open>Abs _\<close>\<close> => true
+  | _ => false;
 
 val nnf_simps = @{thms nnf_simps};
 
@@ -436,21 +436,21 @@
 
   (* FIXME : copied from cqe.ML -- complex QE*)
 fun conjuncts ct =
- case Thm.term_of ct of
-  \<^term>\<open>HOL.conj\<close>$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
-| _ => [ct];
+  case Thm.term_of ct of
+    \<^Const_>\<open>conj for _ _\<close> => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+  | _ => [ct];
 
 fun fold1 f = foldr1 (uncurry f);
 
 fun mk_conj_tab th =
- let fun h acc th =
-   case Thm.prop_of th of
-   \<^term>\<open>Trueprop\<close>$(\<^term>\<open>HOL.conj\<close>$_$_) =>
-     h (h acc (th RS conjunct2)) (th RS conjunct1)
-  | \<^term>\<open>Trueprop\<close>$p => (p,th)::acc
-in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
+  let fun h acc th =
+    case Thm.prop_of th of
+      \<^Const_>\<open>Trueprop for \<^Const_>\<open>conj for _ _\<close>\<close> =>
+        h (h acc (th RS conjunct2)) (th RS conjunct1)
+    | \<^Const_>\<open>Trueprop for p\<close> => (p,th)::acc
+  in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
 
-fun is_conj (\<^term>\<open>HOL.conj\<close>$_$_) = true
+fun is_conj \<^Const_>\<open>conj for _ _\<close> = true
   | is_conj _ = false;
 
 fun prove_conj tab cjs =
@@ -474,11 +474,11 @@
 
    (* Conversion for the equivalence of existential statements where
       EX quantifiers are rearranged differently *)
-fun ext ctxt T = Thm.cterm_of ctxt (Const (\<^const_name>\<open>Ex\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
+fun ext ctxt T = Thm.cterm_of ctxt \<^Const>\<open>Ex T\<close>
 fun mk_ex ctxt v t = Thm.apply (ext ctxt (Thm.typ_of_cterm v)) (Thm.lambda v t)
 
 fun choose v th th' = case Thm.concl_of th of
-  \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) =>
+  \<^Const_>\<open>Trueprop for \<^Const_>\<open>Ex _ for _\<close>\<close> =>
    let
     val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
     val T = Thm.dest_ctyp0 (Thm.ctyp_of_cterm p)
@@ -488,7 +488,7 @@
           (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply p v))
     val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
    in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
-| _ => error ""  (* FIXME ? *)
+  | _ => error ""  (* FIXME ? *)
 
 fun simple_choose ctxt v th =
    choose v (Thm.assume ((Thm.apply \<^cterm>\<open>Trueprop\<close> o mk_ex ctxt v)
@@ -734,7 +734,7 @@
   fun mk_forall x p =
     let
       val T = Thm.typ_of_cterm x;
-      val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
+      val all = Thm.cterm_of ctxt \<^Const>\<open>All T\<close>
     in Thm.apply all (Thm.lambda x p) end
   val avs = Cterms.build (Drule.add_frees_cterm tm)
   val P' = fold mk_forall (Cterms.list_set_rev avs) tm
@@ -753,7 +753,7 @@
         (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [not_ex RS sym])
           (th2 |> Thm.cprop_of)) th2
     in specl (Cterms.list_set_rev avs)
-             ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD)
+             ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS @{thm notnotD})
    end
  end
 fun ideal tms tm ord =
@@ -890,18 +890,18 @@
 
 fun find_term tm ctxt =
   (case Thm.term_of tm of
-    Const (\<^const_name>\<open>HOL.eq\<close>, T) $ _ $ _ =>
-      if domain_type T = HOLogic.boolT then find_args tm ctxt
+    \<^Const_>\<open>HOL.eq T for _ _\<close> =>
+      if T = \<^Type>\<open>bool\<close> then find_args tm ctxt
       else (Thm.dest_arg tm, ctxt)
-  | Const (\<^const_name>\<open>Not\<close>, _) $ _ => find_term (Thm.dest_arg tm) ctxt
-  | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body (Thm.dest_arg tm) ctxt
-  | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body (Thm.dest_arg tm) ctxt
-  | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args tm ctxt
-  | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args tm ctxt
-  | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args tm ctxt
-  | \<^term>\<open>Pure.imp\<close> $_$_ => find_args tm ctxt
+  | \<^Const_>\<open>Not for _\<close> => find_term (Thm.dest_arg tm) ctxt
+  | \<^Const_>\<open>All _ for _\<close> => find_body (Thm.dest_arg tm) ctxt
+  | \<^Const_>\<open>Ex _ for _\<close> => find_body (Thm.dest_arg tm) ctxt
+  | \<^Const_>\<open>conj for _ _\<close> => find_args tm ctxt
+  | \<^Const_>\<open>disj for _ _\<close> => find_args tm ctxt
+  | \<^Const_>\<open>implies for _ _\<close> => find_args tm ctxt
+  | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args tm ctxt
   | Const("(==)",_)$_$_ => find_args tm ctxt  (* FIXME proper const name *)
-  | \<^term>\<open>Trueprop\<close>$_ => find_term (Thm.dest_arg tm) ctxt
+  | \<^Const_>\<open>Trueprop for _\<close> => find_term (Thm.dest_arg tm) ctxt
   | _ => raise TERM ("find_term", []))
 and find_args tm ctxt =
   let val (t, u) = Thm.dest_binop tm
@@ -942,9 +942,11 @@
         | THM _ => no_tac);
 
 local
- fun lhs t = case Thm.term_of t of
-  Const(\<^const_name>\<open>HOL.eq\<close>,_)$_$_ => Thm.dest_arg1 t
- | _=> raise CTERM ("ideal_tac - lhs",[t])
+ fun lhs t =
+   case Thm.term_of t of
+     \<^Const_>\<open>HOL.eq _ for _ _\<close> => Thm.dest_arg1 t
+   | _=> raise CTERM ("ideal_tac - lhs",[t])
+
  fun exitac _ NONE = no_tac
    | exitac ctxt (SOME y) =
       resolve_tac ctxt [Thm.instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
diff -r f3c9203d82c3 -r 41cdf0fb32fa src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Sun Aug 18 14:22:21 2024 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Sun Aug 18 14:40:49 2024 +0200
@@ -128,17 +128,17 @@
   let
     fun numeral_is_const ct =
       case Thm.term_of ct of
-       Const (\<^const_name>\<open>Rings.divide\<close>,_) $ a $ b =>
-         can HOLogic.dest_number a andalso can HOLogic.dest_number b
-     | Const (\<^const_name>\<open>Fields.inverse\<close>,_)$t => can HOLogic.dest_number t
-     | t => can HOLogic.dest_number t
-    fun dest_const ct = ((case Thm.term_of ct of
-       Const (\<^const_name>\<open>Rings.divide\<close>,_) $ a $ b=>
-        Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
-     | Const (\<^const_name>\<open>Fields.inverse\<close>,_)$t =>
-                   Rat.inv (Rat.of_int (snd (HOLogic.dest_number t)))
-     | t => Rat.of_int (snd (HOLogic.dest_number t)))
-       handle TERM _ => error "ring_dest_const")
+        \<^Const_>\<open>divide _ for a b\<close> =>
+          can HOLogic.dest_number a andalso can HOLogic.dest_number b
+      | \<^Const_>\<open>inverse _ for t\<close> => can HOLogic.dest_number t
+      | t => can HOLogic.dest_number t
+    fun dest_const ct =
+      (case Thm.term_of ct of
+          \<^Const_>\<open>divide _ for a b\<close> =>
+            Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+      | \<^Const_>\<open>inverse _ for t\<close> => Rat.inv (Rat.of_int (snd (HOLogic.dest_number t)))
+      | t => Rat.of_int (snd (HOLogic.dest_number t)))
+      handle TERM _ => error "ring_dest_const"
     fun mk_const cT x =
       let val (a, b) = Rat.dest x
       in if b = 1 then Numeral.mk_cnumber cT a