# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID ff5e900d7b1a065a4445a40898ea6c3a0902cb9f
# Parent  e6cffd467ff5cf776ef07036be335ba2d291d152
avoid dumping definitions several times in LEO-II proofs

diff -r e6cffd467ff5 -r ff5e900d7b1a src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- 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
diff -r e6cffd467ff5 -r ff5e900d7b1a src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- 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