changeset 81954 | 6f2bcdfa9a19 |
parent 81254 | d3c0734059ee |
--- a/src/HOL/Tools/Meson/meson.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Wed Jan 22 22:22:19 2025 +0100 @@ -558,7 +558,7 @@ #> let_simps ? rewrite_rule ctxt @{thms Let_def [abs_def]} fun make_nnf simp_options ctxt th = - (case Thm.prems_of th of + (case Thm.take_prems_of 1 th of [] => th |> presimplify simp_options ctxt |> make_nnf1 ctxt | _ => raise THM ("make_nnf: premises in argument", 0, [th]));