# 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