# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID 5b87cfc300f92ca1c1202072f6778d22137b443a
# Parent  ff5e900d7b1a065a4445a40898ea6c3a0902cb9f
add missing timeout multiplier

diff -r ff5e900d7b1a -r 5b87cfc300f9 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Jun 06 10:35:05 2012 +0200
@@ -212,7 +212,7 @@
           (prover ^
            (if aggressivity > 0 then "(" ^ string_of_int aggressivity ^ ")"
             else ""))
-          (atp_tac ctxt aggressivity [] (timeout div frac) prover i)
+          (atp_tac ctxt aggressivity [] (mult * timeout div frac) prover i)
   in
     slice 2 0 ATP_Systems.spassN
     ORELSE slice 2 0 ATP_Systems.vampireN