| changeset 81941 | cb8f396dd39f |
| parent 81519 | cdc43c0fdbfc |
| child 82641 | d22294b20573 |
--- 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