changeset 37628 | 78334f400ae6 |
parent 37619 | bcb19259f92a |
child 38016 | 135f7d489492 |
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jun 29 10:36:36 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jun 29 10:56:45 2010 +0200 @@ -18,7 +18,7 @@ let val thy = ProofContext.theory_of ctxt val ctxt0 = Classical.put_claset HOL_cs ctxt - in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end + in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy false) ths) end val setup = Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>