diff -r d82c0dd51794 -r 05f3af00cc7e src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Mon Mar 22 09:54:22 2010 +0100
+++ b/src/HOL/Tools/meson.ML	Mon Mar 22 10:25:44 2010 +0100
@@ -18,6 +18,7 @@
   val make_nnf: Proof.context -> thm -> thm
   val skolemize: Proof.context -> thm -> thm
   val is_fol_term: theory -> term -> bool
+  val make_clauses_unsorted: thm list -> thm list
   val make_clauses: thm list -> thm list
   val make_horns: thm list -> thm list
   val best_prolog_tac: (thm -> int) -> thm list -> tactic
@@ -560,7 +561,8 @@
 
 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   The resulting clauses are HOL disjunctions.*)
-fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
+fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
+val make_clauses = sort_clauses o make_clauses_unsorted;
 
 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
 fun make_horns ths =