--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Mar 19 16:04:15 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Mar 22 10:25:07 2010 +0100
@@ -463,7 +463,8 @@
fun neg_skolemize_tac ctxt =
EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
-val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
+val neg_clausify =
+ Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf;
fun neg_conjecture_clauses ctxt st0 n =
let