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