# 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