src/HOL/Tools/res_atp.ML
changeset 18798 ca02a2077955
parent 18753 aa82bd41555d
child 18863 a113b6839df1
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Jan 27 18:29:11 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Jan 27 18:29:33 2006 +0100
     1.3 @@ -74,8 +74,8 @@
     1.4  fun dfg_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) = 
     1.5      let val clss = ResClause.make_conjecture_clauses (map prop_of ths)
     1.6          (*FIXME: classrel_clauses and arity_clauses*)
     1.7 -        val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n)
     1.8 -                        axclauses [] [] []    
     1.9 +        val probN = ResClause.clauses2dfg (!problem_name ^ "_" ^ Int.toString n)
    1.10 +                        axclauses clss 
    1.11  	val out = TextIO.openOut(pf n)
    1.12      in
    1.13  	writeln_strs out [probN]; TextIO.closeOut out
    1.14 @@ -106,14 +106,14 @@
    1.15                    val spass = helper_path "SPASS_HOME" "SPASS"
    1.16              in 
    1.17                  ([("spass", spass, infopts ^ baseopts, probfile)] @ 
    1.18 -                  (make_atp_list xs (n+1)))
    1.19 +                  make_atp_list xs (n+1))
    1.20                end
    1.21              else if !prover = "vampire"
    1.22  	    then 
    1.23                let val vampire = helper_path "VAMPIRE_HOME" "vampire"
    1.24                in
    1.25                  ([("vampire", vampire, "-m 100000%-t " ^ time, probfile)] @
    1.26 -                 (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
    1.27 +                 make_atp_list xs (n+1))       (*BEWARE! spaces in options!*)
    1.28                end
    1.29        	     else if !prover = "E"
    1.30        	     then
    1.31 @@ -122,7 +122,7 @@
    1.32  		  ([("E", Eprover, 
    1.33  		     "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
    1.34  		     probfile)] @
    1.35 -		   (make_atp_list xs (n+1)))
    1.36 +		   make_atp_list xs (n+1))
    1.37  	       end
    1.38  	     else error ("Invalid prover name: " ^ !prover)
    1.39            end