src/HOL/Tools/res_atp.ML
changeset 19352 1a07f6cf1e6c
parent 19227 d15f2baa7ecc
child 19442 ad8bb8346e51
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Apr 07 03:20:34 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Apr 07 05:12:00 2006 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4  	val hyp_cls = map prop_of (cnf_hyps_thms ctxt)
     1.5  	val goal_cls = conj_cls@hyp_cls
     1.6  	val user_rules = map ResAxioms.pairname user_thms
     1.7 -	val (names_arr,axclauses_as_tms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
     1.8 +	val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
     1.9  	val thy = ProofContext.theory_of ctxt
    1.10  	val prob_logic = case mode of Auto => problem_logic_goals [goal_cls]
    1.11  				    | Fol => FOL
    1.12 @@ -375,7 +375,7 @@
    1.13  	val writer = tptp_writer
    1.14  	val file = atp_input_file()
    1.15      in
    1.16 -	(writer prob_logic goal_cls file (axclauses_as_tms,classrel_clauses,arity_clauses);
    1.17 +	(writer prob_logic goal_cls file (axclauses_as_thms,classrel_clauses,arity_clauses);
    1.18  	 warning ("Writing to " ^ file);
    1.19  	 file)
    1.20      end;