--- a/src/HOL/Statespace/state_space.ML Tue Jan 21 16:09:51 2025 +0100
+++ b/src/HOL/Statespace/state_space.ML Tue Jan 21 16:12:27 2025 +0100
@@ -349,7 +349,7 @@
val assume =
((Binding.name dist_thm_name, [attr]),
- [(HOLogic.Trueprop $
+ [(HOLogic.mk_Trueprop
(Const (\<^const_name>\<open>all_distinct\<close>, Type (\<^type_name>\<open>tree\<close>, [nameT]) --> HOLogic.boolT) $
DistinctTreeProver.mk_tree (fn n => Free (n, nameT)) nameT
(sort fast_string_ord all_comps)), [])]);
--- a/src/HOL/Tools/Function/induction_schema.ML Tue Jan 21 16:09:51 2025 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Tue Jan 21 16:12:27 2025 +0100
@@ -141,7 +141,7 @@
end
fun mk_wf R (IndScheme {T, ...}) =
- HOLogic.Trueprop $ (Const (\<^const_abbrev>\<open>wf\<close>, mk_relT T --> HOLogic.boolT) $ R)
+ HOLogic.mk_Trueprop (Const (\<^const_abbrev>\<open>wf\<close>, mk_relT T --> HOLogic.boolT) $ R)
fun mk_ineqs R thesisn (IndScheme {T, cases, branches}) =
let
--- a/src/HOL/Tools/Function/mutual.ML Tue Jan 21 16:09:51 2025 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Tue Jan 21 16:12:27 2025 +0100
@@ -184,7 +184,7 @@
val simp_ctxt = fold Thm.declare_hyps (Thm.chyps_of simp) ctxt
in
Goal.prove simp_ctxt [] []
- (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (f, args), rhs)))
(fn _ =>
Local_Defs.unfold0_tac ctxt all_orig_fdefs
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1