Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Metis/metis_tactic.ML
changeset 51717 9e7d1c139569
parent 50875 bfb626265782
child 52031 9a9238342963 
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Apr 18 17:07:01 2013 +0200
@@ -249,7 +249,7 @@
 fun preskolem_tac ctxt st0 =
   (if exists (Meson.has_too_many_clauses ctxt)
              (Logic.prems_of_goal (prop_of st0) 1) then
-     Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
+     Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex} ctxt) 1
      THEN cnf.cnfx_rewrite_tac ctxt 1
    else
      all_tac) st0
isabelle