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