# HG changeset patch
# User blanchet
# Date 1271429645 -7200
# Node ID bd246b00ef5a76514e03ab01df304c1252c0216d
# Parent  0ee736f08ed0d384b8123c4d6df36e2378f52551
restore order of clauses in TPTP output;
there's a rather subtle invariant w.r.t. "extract_lemmas"

diff -r 0ee736f08ed0 -r bd246b00ef5a src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- 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;