--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jun 06 10:35:05 2012 +0200
@@ -201,9 +201,11 @@
isa_ext
fun add_all_defs fact_names accum =
- Vector.foldl (fn (facts, factss) =>
- filter (fn (_, (_, status)) => status = Def) facts @ factss)
- accum fact_names
+ Vector.foldl
+ (fn (facts, facts') =>
+ union (op =) (filter (fn (_, (_, status)) => status = Def) facts)
+ facts')
+ accum fact_names
fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) =
(if rule = leo2_ext then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jun 06 10:35:05 2012 +0200
@@ -38,8 +38,7 @@
let val n = length names in
string_of_int n ^ " fact" ^ plural_s n ^
(if n > 0 then
- ": " ^ (names |> map fst |> sort_distinct string_ord
- |> space_implode " ")
+ ": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
else
"")
end