--- 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 **)
--- 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