src/HOL/Tools/res_atp.ML
changeset 20131 c89ee2f4efd5
parent 20022 b07a138b4e7d
child 20224 9c40a144ee0e
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sat Jul 15 13:50:26 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Sat Jul 15 13:52:10 2006 +0200
     1.3 @@ -586,15 +586,15 @@
     1.4  
     1.5  val linkup_logic_mode = ref Auto;
     1.6  
     1.7 -fun tptp_writer logic goals filename (axioms,classrels,arities) =
     1.8 +fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
     1.9      if is_fol_logic logic 
    1.10      then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
    1.11 -    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities);
    1.12 +    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
    1.13  
    1.14 -fun dfg_writer logic goals filename (axioms,classrels,arities) =
    1.15 +fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
    1.16      if is_fol_logic logic 
    1.17      then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
    1.18 -    else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities);
    1.19 +    else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
    1.20  
    1.21  (*Called by the oracle-based methods declared in res_atp_methods.ML*)
    1.22  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
    1.23 @@ -602,6 +602,7 @@
    1.24  	val hyp_cls = cnf_hyps_thms ctxt
    1.25  	val goal_cls = conj_cls@hyp_cls
    1.26  	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
    1.27 +	val user_lemmas_names = map #1 user_rules
    1.28  	val rm_black_cls = blacklist_filter included_thms 
    1.29  	val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls
    1.30  	val user_cls = ResAxioms.cnf_rules_pairs user_rules
    1.31 @@ -618,7 +619,7 @@
    1.32          val writer = if dfg then dfg_writer else tptp_writer 
    1.33  	val file = atp_input_file()
    1.34      in
    1.35 -	(writer prob_logic goal_cls file (axclauses,classrel_clauses,arity_clauses);
    1.36 +	(writer prob_logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
    1.37  	 Output.debug ("Writing to " ^ file);
    1.38  	 file)
    1.39      end;
    1.40 @@ -734,7 +735,7 @@
    1.41        val writer = if !prover = "spass" then dfg_writer else tptp_writer 
    1.42        fun write_all [] _ = []
    1.43  	| write_all (sub::subgoals) k =
    1.44 -	   (writer goals_logic sub (probfile k) (axclauses,classrel_clauses,arity_clauses),
    1.45 +	   (writer goals_logic sub (probfile k) (axclauses,classrel_clauses,arity_clauses) [],
    1.46  	    probfile k) :: write_all subgoals (k-1)
    1.47        val (clnames::_, filenames) = ListPair.unzip (write_all neg_subgoals (length goals))
    1.48        val thm_names = Array.fromList clnames