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;