src/HOL/Tools/res_atp.ML
changeset 16259 aed1a8ae4b23
parent 16185 bb71c91e781e
child 16357 f1275d2a1dee
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sun Jun 05 11:31:21 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Sun Jun 05 11:31:22 2005 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4  	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
     1.5  	val tfree_lits = ResLib.flat_noDup tfree_litss
     1.6  	val tfree_clss = map ResClause.tfree_clause tfree_lits 
     1.7 -        val hypsfile = File.sysify_path hyps_file
     1.8 +        val hypsfile = File.platform_path hyps_file
     1.9  	val out = TextIO.openOut(hypsfile)
    1.10      in
    1.11  	((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits) 
    1.12 @@ -127,7 +127,7 @@
    1.13          val _ = (warning ("in tptp_inputs_tfrees 2"))
    1.14  	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
    1.15           val _ = (warning ("in tptp_inputs_tfrees 3"))
    1.16 -        val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    1.17 +        val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    1.18  	val out = TextIO.openOut(probfile)
    1.19      in
    1.20  	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out;
    1.21 @@ -168,11 +168,11 @@
    1.22  	val no_returns =List.filter   not_newline ( thmproofstring)
    1.23  	val thmstr = implode no_returns
    1.24         
    1.25 -	val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    1.26 -	val axfile = (File.sysify_path axiom_file)
    1.27 -	val hypsfile = (File.sysify_path hyps_file)
    1.28 -	val clasimpfile = (File.sysify_path clasimp_file)
    1.29 -	val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile")))
    1.30 +	val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    1.31 +	val axfile = (File.platform_path axiom_file)
    1.32 +	val hypsfile = (File.platform_path hyps_file)
    1.33 +	val clasimpfile = (File.platform_path clasimp_file)
    1.34 +	val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "hellofile")))
    1.35  	val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
    1.36  	val _ = TextIO.flushOut outfile;
    1.37  	val _ =  TextIO.closeOut outfile
    1.38 @@ -298,9 +298,9 @@
    1.39          
    1.40  	(* set up variables for writing out the clasimps to a tptp file *)
    1.41  	val (clause_arr, num_of_clauses) =
    1.42 -	    ResClasimp.write_out_clasimp (File.sysify_path clasimp_file) 
    1.43 +	    ResClasimp.write_out_clasimp (File.platform_path clasimp_file) 
    1.44  	                                 (ProofContext.theory_of ctxt)
    1.45 -        val _ = warning ("clasimp_file is " ^ File.sysify_path clasimp_file)
    1.46 +        val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file)
    1.47  
    1.48          (* cq: add write out clasimps to file *)
    1.49  
    1.50 @@ -375,7 +375,7 @@
    1.51  	val thms_ss = get_thms_ss delta_ss_thms
    1.52  	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
    1.53  	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
    1.54 -	val ax_file = File.sysify_path axiom_file
    1.55 +	val ax_file = File.platform_path axiom_file
    1.56  	val out = TextIO.openOut ax_file
    1.57      in
    1.58  	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)