src/HOL/Tools/Meson/meson.ML
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]));