changeset 42336 | d63d43e85879 |
parent 40665 | 1a65f0c74827 |
child 42341 | 5a00af7f4978 |
--- 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