# HG changeset patch
# User blanchet
# Date 1302773044 -7200
# Node ID d63d43e858793ba226edf5a06359f617a746e12e
# Parent  cb8aa792d138051397ea7376cdf415939d24fb19
improve definitional CNF on goal by moving "not" past the quantifiers

diff -r cb8aa792d138 -r d63d43e85879 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Apr 14 11:24:04 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Apr 14 11:24:04 2011 +0200
@@ -15,6 +15,7 @@
   val introduce_combinators_in_theorem : thm -> thm
   val to_definitional_cnf_with_quantifiers : Proof.context -> thm -> thm
   val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
+  val ss_only : thm list -> simpset
   val cnf_axiom :
     Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
 end;
diff -r cb8aa792d138 -r d63d43e85879 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Apr 14 11:24:04 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Apr 14 11:24:04 2011 +0200
@@ -142,7 +142,8 @@
 fun preskolem_tac ctxt st0 =
   (if exists (Meson.has_too_many_clauses ctxt)
              (Logic.prems_of_goal (prop_of st0) 1) then
-     cnf.cnfx_rewrite_tac ctxt 1
+     Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
+     THEN cnf.cnfx_rewrite_tac ctxt 1
    else
      all_tac) st0