# HG changeset patch
# User blanchet
# Date 1307545267 -7200
# Node ID 755e3d5ea3f2d6a1e5840b1798d361b485d16e35
# Parent  30aaab778416c8c31f4049a4d27485838fd3c4ba
avoid duplicate facts, which confuse the minimizer output

diff -r 30aaab778416 -r 755e3d5ea3f2 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 08 16:20:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 08 17:01:07 2011 +0200
@@ -225,7 +225,7 @@
   | add_fact _ _ _ _ _ = I
 
 fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof =
-  if null atp_proof then Vector.foldl (op @) [] fact_names
+  if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
   else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof []
 
 fun is_conjecture_used_in_proof conjecture_shape =