# HG changeset patch
# User blanchet
# Date 1344337430 -7200
# Node ID 62928b793d8a3fd9411ba1013d1067f8c0aa3676
# Parent  56b633faec9934c6766555a304b67bc8a917f6fd
specify full path to clausifier

diff -r 56b633faec99 -r 62928b793d8a src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 07 11:25:01 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 07 13:03:50 2012 +0200
@@ -355,7 +355,7 @@
 val iprover_config : atp_config =
   {exec = (["IPROVER_HOME"], ["iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
-       "--clausifier vclausify_rel --time_out_real " ^
+       "--clausifier $IPROVER_HOME/vclausify_rel --time_out_real " ^
        string_of_real (Time.toReal timeout),
    proof_delims = tstp_proof_delims,
    known_failures =