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