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