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 55239 97921d23ebe3
parent 55236 8d61b0aa7a0d
child 55257 abfd7b90bba2 
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Sat Feb 01 20:46:19 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sat Feb 01 21:09:53 2014 +0100
@@ -245,7 +245,7 @@
   (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} ctxt) 1
-     THEN cnf.cnfx_rewrite_tac ctxt 1
+     THEN CNF.cnfx_rewrite_tac ctxt 1
    else
      all_tac) st0
isabelle