--- 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
--- 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);
--- 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,
--- 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