# HG changeset patch # User blanchet # Date 1677654051 -3600 # Node ID 110988ad5b4cdfe196d5a466d03c775a784e6831 # Parent 7c76221baecbd2906f80d3e3a0a8c1b0118a46a0 compile diff -r 7c76221baecb -r 110988ad5b4c src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed Mar 01 08:00:51 2023 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Mar 01 08:00:51 2023 +0100 @@ -57,7 +57,7 @@ val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = space_implode " " (File.bash_path (Path.explode path) :: - arguments ctxt false "" atp_timeout prob_file) + arguments false false "" atp_timeout prob_file) val outcome = Timeout.apply atp_timeout Isabelle_System.bash_output command |> fst