restore order of clauses in TPTP output;
there's a rather subtle invariant w.r.t. "extract_lemmas"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Apr 16 16:53:00 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Apr 16 16:54:05 2010 +0200
@@ -502,10 +502,10 @@
         "% " ^ timestamp () ^ "\n" ::
         section "Relevant fact" ax_clss @
         section "Type variable" tfree_clss @
+        section "Conjecture" conjecture_clss @
         section "Class relationship" classrel_clss @
         section "Arity declaration" arity_clss @
-        section "Helper fact" helper_clss @
-        section "Conjecture" conjecture_clss)
+        section "Helper fact" helper_clss)
     in (length axclauses + 1, length tfree_clss + length conjecture_clss)
   end;