src/HOL/TPTP/MaSh_Export.thy

--- a/src/HOL/TPTP/MaSh_Export.thy	Mon Jun 02 11:59:49 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Mon Jun 02 11:59:50 2014 +0200
@@ -14,6 +14,7 @@
   [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
    lam_trans = lifting, timeout = 2, dont_preplay, minimize]
 
+declare [[sledgehammer_fact_duplicates = true]]
 declare [[sledgehammer_instantiate_inducts = false]]
 
 hide_fact (open) HOL.ext