src/HOL/Tools/res_atp.ML

 	else if File.exists (File.unpack_platform_path (!destdir))
 	then !destdir ^ "/" ^ file
 	else error ("No such directory: " ^ !destdir)
     end;
 
-val include_all = ref false;
+val include_all = ref true;
 val include_simpset = ref false;
 val include_claset = ref false; 
 val include_atpset = ref true;
 
 (*Tests show that follow_defs gives VERY poor results with "include_all"*)

 fun mk_clause_table n =
       Polyhash.mkTable (hash_term o prop_of, equal_thm)
                        (n, HASH_CLAUSE);
 
 (*Use a hash table to eliminate duplicates from xs. Argument is a list of
-  (name, theorem) pairs, but the theorems are hashed into the table. *)
+  (thm * (string * int)) tuples. The theorems are hashed into the table. *)
 fun make_unique xs = 
+  let val ht = mk_clause_table 7000
+  in
+      app (ignore o Polyhash.peekInsert ht) xs;  
+      Polyhash.listItems ht
+  end;
+
+(*Remove existing axiom clauses from the conjecture clauses, as this can dramatically
+  boost an ATP's performance (for some reason)*)
+fun subtract_cls c_clauses ax_clauses = 
   let val ht = mk_clause_table 2200
+      fun known x = isSome (Polyhash.peek ht x)
   in
-      (app (ignore o Polyhash.peekInsert ht) (map swap xs);  
-       map swap (Polyhash.listItems ht))
+      app (ignore o Polyhash.peekInsert ht) ax_clauses;  
+      filter (not o known) c_clauses 
   end;
 
-(*FIXME: SLOW!!!*)
-fun mem_thm th [] = false
-  | mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names;
-
-(*FIXME: SLOW!!! These two functions are called only by get_relevant_clauses.
-  It would be faster to compare names, rather than theorems, and to use
-  a symbol table or hash table.*)
-fun insert_thms [] thms_names = thms_names
-  | insert_thms ((thm,name)::thms_names) thms_names' =
-      if mem_thm thm thms_names' then insert_thms thms_names thms_names' 
-      else insert_thms thms_names ((thm,name)::thms_names');
-
-(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
+(*Filter axiom clauses, but keep supplied clauses and clauses in whitelist. 
+  Duplicates are removed later.*)
 fun get_relevant_clauses thy cls_thms white_cls goals =
-  insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);
+  white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
 
 (*This name is cryptic but short. Unlike gensym, we get the same name each time.*)
 fun fake_thm_name th = 
     Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th);
 

                             Auto => problem_logic_goals [map prop_of goal_cls]
 			  | Fol => FOL
 			  | Hol => HOL
 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
 	val cla_simp_atp_clauses = included_thms |> blacklist_filter
-	                             |> make_unique |> ResAxioms.cnf_rules_pairs
+	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
                                      |> restrict_to_logic logic 
 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
 	val thy = ProofContext.theory_of ctxt
 	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
-	                            user_cls (map prop_of goal_cls)
+	                            user_cls (map prop_of goal_cls) |> make_unique
 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
 	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
         val writer = if dfg then dfg_writer else tptp_writer 
 	and file = atp_input_file()

 		Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
 	      | Fol => FOL
 	      | Hol => HOL
       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
       val included_cls = included_thms |> blacklist_filter
-                                       |> make_unique |> ResAxioms.cnf_rules_pairs 
+                                       |> ResAxioms.cnf_rules_pairs |> make_unique 
                                        |> restrict_to_logic logic 
       val white_cls = ResAxioms.cnf_rules_pairs white_thms
       (*clauses relevant to goal gl*)
       val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
                            goals

                           else []
       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
       val writer = if !prover = "spass" then dfg_writer else tptp_writer 
       fun write_all [] [] _ = []
 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
-	   (writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [],
-	    probfile k) 
-	   :: write_all ccls_list axcls_list (k+1)
+            let val fname = probfile k
+                val axcls = make_unique axcls
+                val ccls = subtract_cls ccls axcls
+                val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
+            in  (clnames,fname) :: write_all ccls_list axcls_list (k+1)  end
       val (clnames::_, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
       val thm_names = Array.fromList clnames
       val _ = if !Output.show_debug_msgs 
               then trace_array "thm_names" thm_names else ()
   in