# HG changeset patch
# User mengj
# Date 1132294067 -3600
# Node ID 082a2bd6f655a8d246d839f0ac50550b3f29b76e
# Parent  02f1c40224846aadd15c0240a4538adf3d985ac1
-- added combinator reduction axioms (typed and untyped) for HOL goals.
-- combined make_nnf functions for HOL and FOL goals.
-- hypothesis of goals are now also skolemized by inference.

diff -r 02f1c4022484 -r 082a2bd6f655 src/HOL/Tools/res_atp_setup.ML
--- a/src/HOL/Tools/res_atp_setup.ML	Fri Nov 18 07:07:06 2005 +0100
+++ b/src/HOL/Tools/res_atp_setup.ML	Fri Nov 18 07:07:47 2005 +0100
@@ -14,6 +14,22 @@
 (* set up the output paths                             *)
 (*******************************************************)
 
+fun typed_comb () = 
+    if !ResHolClause.include_combS then 
+	(ResAtp.helper_path "E_HOME" "additionals/comb_inclS"
+	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/comb_inclS")
+    else 
+	(ResAtp.helper_path "E_HOME" "additionals/comb_noS"
+	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/comb_noS");
+
+fun untyped_comb () = 
+    if !ResHolClause.include_combS then 
+	(ResAtp.helper_path "E_HOME" "additionals/u_comb_inclS"
+	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS")
+    else
+	(ResAtp.helper_path "E_HOME" "additionals/u_comb_noS"
+	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_comb_noS");
+
 val claset_file = File.tmp_path (Path.basic "claset");
 val simpset_file = File.tmp_path (Path.basic "simp");
 val local_lemma_file = File.tmp_path (Path.basic "locallemmas");
@@ -101,12 +117,9 @@
 
 fun tptp_hyps_g _ [] = ([], [])
   | tptp_hyps_g is_fol thms =
-    let val mk_nnf = if is_fol then make_nnf else make_nnf1
-	val prems = map (skolemize o mk_nnf o ObjectLogic.atomize_thm) thms
-        val prems' = map repeat_someI_ex prems
-        val prems'' = make_clauses prems'
-        val prems''' = map prop_of prems''  (*FIXME: was rm_Eps*)
-	val (tptp_clss,tfree_litss) = mk_conjectures is_fol prems'''
+    let val prems = ResClause.union_all (map ResAxioms.cnf_axiom_aux thms)
+	val prems' = map prop_of prems
+	val (tptp_clss,tfree_litss) = mk_conjectures is_fol prems'
 	val tfree_lits = ResClause.union_all tfree_litss
 	val tfree_clss = map ResClause.tfree_clause tfree_lits 
         val hypsfile = File.platform_path hyps_file
@@ -205,19 +218,23 @@
 (***************************************************************)
 (* setup ATPs as Isabelle methods                              *)
 (***************************************************************)
-fun atp_meth_g tptp_hyps tptp_cnf_clasimp tac ths ctxt = 
+fun atp_meth_g helper_file tptp_hyps tptp_cnf_clasimp tac ths ctxt = 
     let val rules = if !filter_ax then find_relevant_ax tptp_cnf_clasimp ths ctxt 
 		    else tptp_cnf_clasimp ths ctxt (!include_claset, !include_simpset) 
 	val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt)
 	val thy = ProofContext.theory_of ctxt
 	val tsfile = tptp_types_sorts thy
-	val files = hyps @ rules @ tsfile
+	val files = (helper_file,hyps @ rules @ tsfile)
     in
 	Method.SIMPLE_METHOD' HEADGOAL
 	(tac ctxt files tfrees)
     end;
-fun atp_meth_f tac ths ctxt = atp_meth_g tptp_hyps tptp_cnf_clasimp tac ths ctxt;
-fun atp_meth_h tac ths ctxt = atp_meth_g tptp_hypsH tptp_cnf_clasimpH tac ths ctxt;
+fun atp_meth_f tac ths ctxt = atp_meth_g [] tptp_hyps tptp_cnf_clasimp tac ths ctxt;
+fun atp_meth_h tac ths ctxt = 
+    let val helper = if !ResHolClause.keep_types then [typed_comb ()] else [untyped_comb ()]
+    in
+	atp_meth_g helper tptp_hypsH tptp_cnf_clasimpH tac ths ctxt
+    end;
 
 
 fun atp_meth_G atp_meth tac ths ctxt =