# HG changeset patch
# User wenzelm
# Date 1723036314 -7200
# Node ID ad9647592a81012f868fb6e8c96bcda9cc3811db
# Parent  231d58c412b53f0b2f4b276abe5ac5688bc300e7
tuned: more antiquotations;

diff -r 231d58c412b5 -r ad9647592a81 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Aug 07 14:44:51 2024 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Aug 07 15:11:54 2024 +0200
@@ -199,12 +199,12 @@
   val Eq_TrueI = @{thm Eq_TrueI}
 
   fun is_subset A th = case Thm.prop_of th of
-        (_ $ (Const (\<^const_name>\<open>less_eq\<close>, Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>set\<close>, _), _])) $ A' $ B))
+        (_ $ \<^Const_>\<open>less_eq \<^Type>\<open>set _\<close> for A' B\<close>)
         => if A aconv A' then SOME(B,th) else NONE
       | _ => NONE;
 
   fun is_finite th = case Thm.prop_of th of
-        (_ $ (Const (\<^const_name>\<open>finite\<close>, _) $ A)) => SOME(A,th)
+        (_ $ \<^Const_>\<open>finite _ for A\<close>) => SOME(A,th)
       |  _ => NONE;
 
   fun comb (A,sub_th) (A',fin_th) ths = if A aconv A' then (sub_th,fin_th) :: ths else ths
diff -r 231d58c412b5 -r ad9647592a81 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Aug 07 14:44:51 2024 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 07 15:11:54 2024 +0200
@@ -818,11 +818,11 @@
 setup \<open>
   (*prevent substitution on bool*)
   let
-    fun non_bool_eq (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) = T <> \<^typ>\<open>bool\<close>
+    fun non_bool_eq \<^Const_>\<open>HOL.eq T\<close> = T <> \<^Type>\<open>bool\<close>
       | non_bool_eq _ = false;
     fun hyp_subst_tac' ctxt =
       SUBGOAL (fn (goal, i) =>
-        if Term.exists_Const non_bool_eq goal
+        if Term.exists_subterm non_bool_eq goal
         then Hypsubst.hyp_subst_tac ctxt i
         else no_tac);
   in
@@ -1263,7 +1263,7 @@
       | count_loose (s $ t) k = count_loose s k + count_loose t k
       | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
       | count_loose _ _ = 0;
-    fun is_trivial_let (Const (\<^const_name>\<open>Let\<close>, _) $ x $ t) =
+    fun is_trivial_let \<^Const_>\<open>Let _ _ for x t\<close> =
       (case t of
         Abs (_, _, t') => count_loose t' 0 <= 1
       | _ => true);
@@ -1277,7 +1277,7 @@
           val (t', ctxt') = yield_singleton (Variable.import_terms false) t ctxt;
         in
           Option.map (hd o Variable.export ctxt' ctxt o single)
-            (case t' of Const (\<^const_name>\<open>Let\<close>,_) $ x $ f => (* x and f are already in normal form *)
+            (case t' of \<^Const_>\<open>Let _ _ for x f\<close> => (* x and f are already in normal form *)
               if is_Free x orelse is_Bound x orelse is_Const x
               then SOME @{thm Let_def}
               else
@@ -1347,7 +1347,7 @@
         Conv.rewr_conv @{thm HOL.False_implies_equals}
   in
     case concl of
-      Const (@{const_name HOL.Trueprop}, _) $ _ => SOME (go (length prems) ct)
+      \<^Const_>\<open>Trueprop for _\<close> => SOME (go (length prems) ct)
     | _ => NONE
   end
 \<close>
@@ -1536,7 +1536,7 @@
   val rulify = @{thms induct_rulify'}
   val rulify_fallback = @{thms induct_rulify_fallback}
   val equal_def = @{thm induct_equal_def}
-  fun dest_def (Const (\<^const_name>\<open>induct_equal\<close>, _) $ t $ u) = SOME (t, u)
+  fun dest_def \<^Const_>\<open>induct_equal _ for t u\<close> = SOME (t, u)
     | dest_def _ = NONE
   fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
 )
@@ -1937,7 +1937,7 @@
 simproc_setup passive equal (HOL.eq) =
   \<open>fn _ => fn _ => fn ct =>
     (case Thm.term_of ct of
-      Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal}
+      \<^Const_>\<open>HOL.eq T\<close> => if is_Type T then SOME @{thm eq_equal} else NONE
     | _ => NONE)\<close>
 
 setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>equal\<close>])\<close>
@@ -2153,7 +2153,7 @@
 ML \<open>
   (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   local
-    fun wrong_prem (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = wrong_prem t
+    fun wrong_prem \<^Const_>\<open>All _ for \<open>Abs (_, _, t)\<close>\<close> = wrong_prem t
       | wrong_prem (Bound _) = true
       | wrong_prem _ = false;
     val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
diff -r 231d58c412b5 -r ad9647592a81 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Aug 07 14:44:51 2024 +0200
+++ b/src/HOL/Product_Type.thy	Wed Aug 07 15:11:54 2024 +0200
@@ -1334,22 +1334,22 @@
 simproc_setup Collect_mem ("Collect t") = \<open>
   K (fn ctxt => fn ct =>
     (case Thm.term_of ct of
-      S as Const (\<^const_name>\<open>Collect\<close>, Type (\<^type_name>\<open>fun\<close>, [_, T])) $ t =>
+      S as \<^Const_>\<open>Collect A for t\<close> =>
         let val (u, _, ps) = HOLogic.strip_ptupleabs t in
           (case u of
-            (c as Const (\<^const_name>\<open>Set.member\<close>, _)) $ q $ S' =>
+            (c as \<^Const_>\<open>Set.member _ for q S'\<close>) =>
               (case try (HOLogic.strip_ptuple ps) q of
                 NONE => NONE
               | SOME ts =>
                   if not (Term.is_open S') andalso
                     ts = map Bound (length ps downto 0)
                   then
-                    let val simp =
-                      full_simp_tac (put_simpset HOL_basic_ss ctxt
-                        addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1
+                    let
+                      val simp =
+                        full_simp_tac (put_simpset HOL_basic_ss ctxt
+                          addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1
                     in
-                      SOME (Goal.prove ctxt [] []
-                        (Const (\<^const_name>\<open>Pure.eq\<close>, T --> T --> propT) $ S $ S')
+                      SOME (Goal.prove ctxt [] [] \<^Const>\<open>Pure.eq \<^Type>\<open>set A\<close> for S S'\<close>
                         (K (EVERY
                           [resolve_tac ctxt [eq_reflection] 1,
                            resolve_tac ctxt @{thms subset_antisym} 1,
diff -r 231d58c412b5 -r ad9647592a81 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Aug 07 14:44:51 2024 +0200
+++ b/src/HOL/Set.thy	Wed Aug 07 15:11:54 2024 +0200
@@ -251,7 +251,7 @@
       else raise Match;
 
     fun tr' q = (q, fn _ =>
-      (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, Type (\<^type_name>\<open>set\<close>, _)),
+      (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, \<^Type>\<open>set _\<close>),
           Const (c, _) $
             (Const (d, _) $ (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v', T)) $ n) $ P] =>
           (case AList.lookup (=) trans (q, c, d) of