src/HOL/Tools/ATP/watcher.ML
changeset 17121 4c225f640b89
parent 16805 fadf80952202
child 17150 ce2a1aeb42aa
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Aug 18 13:06:05 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Aug 18 13:09:21 2005 +0200
     1.3 @@ -266,9 +266,6 @@
     1.4      val dfg_dir = File.tmp_path (Path.basic "dfg"); 
     1.5      val dfg_path = File.platform_path dfg_dir;
     1.6      
     1.7 -    val tptp2X = ResLib.helper_path "TPTP2X_HOME" "tptp2X"  		
     1.8 -
     1.9 -
    1.10      (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    1.11      val probID = List.last(explode probfile)
    1.12      val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    1.13 @@ -286,7 +283,8 @@
    1.14  	    warning("not converting to dfg")
    1.15      
    1.16      val _ = if !SpassComm.spass then 
    1.17 -		system (tptp2X ^ " -fdfg -d "^dfg_path^" "^
    1.18 +		system (ResLib.helper_path "TPTP2X_HOME" "tptp2X" ^ 
    1.19 +		        " -fdfg -d " ^ dfg_path ^ " " ^
    1.20  			File.platform_path wholefile)
    1.21  	      else 7
    1.22      val newfile =   if !SpassComm.spass