# HG changeset patch
# User blanchet
# Date 1277289789 -7200
# Node ID ef3742657bc6af1e2be1d4d79e7f7bd235b46bf3
# Parent  b147d01b8ebc53564272d7ede7ab0cced99a102d
fix bug with "skolem_id" + sort facts for increased readability

diff -r b147d01b8ebc -r ef3742657bc6 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Jun 23 11:36:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Jun 23 12:43:09 2010 +0200
@@ -175,7 +175,7 @@
       end
     fun do_term (Const x) = do_const x
       | do_term (Free x) = do_const x
-      | do_term (Const (@{const_name skolem_id}, _) $ _) = I
+      | do_term (Const (x as (@{const_name skolem_id}, _)) $ _) = do_const x
       | do_term (t $ u) = do_term t #> do_term u
       | do_term (Abs (_, _, t)) = do_term t
       | do_term _ = I
@@ -574,6 +574,7 @@
                        defs_relevant max_new theory_relevant relevance_override
                        thy axioms (map prop_of goal_cls)
       |> has_override ? make_unique
+      |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
     end
 
 (** Helper clauses **)
diff -r b147d01b8ebc -r ef3742657bc6 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Jun 23 11:36:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Jun 23 12:43:09 2010 +0200
@@ -216,7 +216,7 @@
   in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
 
 fun make_axiom_clauses thy clauses =
-  ([], []) |> fold (add_axiom_clause thy) clauses |> snd
+  ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
 
 fun make_conjecture_clauses thy =
   let