changeset 47953 | a2c3706c4cb1 |
parent 46904 | f30e941b4512 |
child 47954 | aada9fd08b58 |
--- a/src/HOL/Tools/Meson/meson_clausify.ML Mon May 21 16:37:28 2012 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue May 22 16:59:27 2012 +0200 @@ -309,8 +309,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 - |> extensionalize_theorem ctxt - |> make_nnf ctxt + |> abs_extensionalize_thm ctxt |> make_nnf ctxt in if new_skolemizer then let