# HG changeset patch
# User paulson
# Date 1124363361 -7200
# Node ID 4c225f640b890a8467c71ca75baffce05c1d2228
# Parent  4ddeef83bd66e072333d2e2475d1b6f085c6f48c
no need for TPTP2X unless SPASS is used

diff -r 4ddeef83bd66 -r 4c225f640b89 src/HOL/Tools/ATP/watcher.ML
--- a/src/HOL/Tools/ATP/watcher.ML	Thu Aug 18 13:06:05 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Thu Aug 18 13:09:21 2005 +0200
@@ -266,9 +266,6 @@
     val dfg_dir = File.tmp_path (Path.basic "dfg"); 
     val dfg_path = File.platform_path dfg_dir;
     
-    val tptp2X = ResLib.helper_path "TPTP2X_HOME" "tptp2X"  		
-
-
     (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
     val probID = List.last(explode probfile)
     val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
@@ -286,7 +283,8 @@
 	    warning("not converting to dfg")
     
     val _ = if !SpassComm.spass then 
-		system (tptp2X ^ " -fdfg -d "^dfg_path^" "^
+		system (ResLib.helper_path "TPTP2X_HOME" "tptp2X" ^ 
+		        " -fdfg -d " ^ dfg_path ^ " " ^
 			File.platform_path wholefile)
 	      else 7
     val newfile =   if !SpassComm.spass