src/HOL/Tools/Sledgehammer/meson_tactic.ML
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 =>