changeset 46071 | 1613933e412c |
parent 45740 | 132a3e1c0fe5 |
child 46497 | 89ccf66aa73d |
--- a/src/HOL/Tools/Meson/meson_clausify.ML Mon Jan 02 11:54:21 2012 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Jan 02 14:12:20 2012 +0100 @@ -311,7 +311,6 @@ |> 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 ctxt |> make_nnf ctxt in