changeset 42739 | 017e5dac8642 |
parent 42361 | 23f352990944 |
child 42747 | f132d13fcf75 |
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu May 12 15:29:19 2011 +0200 @@ -320,6 +320,7 @@ |> new_skolemizer ? forall_intr_vars val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single val th = th |> Conv.fconv_rule Object_Logic.atomize + |> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt) |> extensionalize_theorem |> make_nnf ctxt in