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