# HG changeset patch
# User wenzelm
# Date 1737472347 -3600
# Node ID cb8f396dd39f87084d5c43b2ab85f616d3463bb6
# Parent  35d243b25ae26d474ab6db6885319123ecf139a0
tuned;

diff -r 35d243b25ae2 -r cb8f396dd39f src/HOL/Statespace/state_space.ML
--- 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)), [])]);
diff -r 35d243b25ae2 -r cb8f396dd39f src/HOL/Tools/Function/induction_schema.ML
--- 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
diff -r 35d243b25ae2 -r cb8f396dd39f src/HOL/Tools/Function/mutual.ML
--- 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