src/HOL/Tools/res_atp.ML
changeset 17888 116a8d1c7a67
parent 17849 d7619ccf22e6
child 18003 2aecb2d68c00
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Oct 17 23:10:25 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 18 15:08:38 2005 +0200
     1.3 @@ -65,9 +65,9 @@
     1.4    | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
     1.5  
     1.6  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
     1.7 -fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
     1.8 +fun tptp_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) =
     1.9    let
    1.10 -    val clss = ResClause.make_conjecture_clauses thms
    1.11 +    val clss = ResClause.make_conjecture_clauses (map prop_of ths)
    1.12      val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    1.13      val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss)
    1.14      val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
    1.15 @@ -80,8 +80,8 @@
    1.16    end;
    1.17  
    1.18  (* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.19 -fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = 
    1.20 -    let val clss = ResClause.make_conjecture_clauses thms
    1.21 +fun dfg_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) = 
    1.22 +    let val clss = ResClause.make_conjecture_clauses (map prop_of ths)
    1.23          (*FIXME: classrel_clauses and arity_clauses*)
    1.24          val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n)
    1.25                          axclauses [] [] []    
    1.26 @@ -91,10 +91,7 @@
    1.27      end;
    1.28  
    1.29  
    1.30 -(*********************************************************************)
    1.31  (* call prover with settings and problem file for the current subgoal *)
    1.32 -(*********************************************************************)
    1.33 -(* now passing in list of skolemized thms and list of sgterms to go with them *)
    1.34  fun watcher_call_provers sign sg_terms (childin, childout, pid) =
    1.35    let
    1.36      fun make_atp_list [] n = []