# HG changeset patch
# User blanchet
# Date 1309175567 -7200
# Node ID dda3e38cc351f23152e86c0bb34017b5cc193398
# Parent  a818d5a34cca674b78c35a663ce9bf9b184bb235
remove experimental trimming feature -- it slowed down things on Linux for some reason

diff -r a818d5a34cca -r dda3e38cc351 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 27 13:52:47 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 27 13:52:47 2011 +0200
@@ -197,10 +197,9 @@
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
    arguments =
-     fn ctxt => fn full_proof => fn method => fn timeout => fn weights =>
+     fn ctxt => fn _ => fn method => fn timeout => fn weights =>
         "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
-        " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout) ^
-        (if full_proof orelse is_old_e_version () then "" else " --trim"),
+        " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
      [(Unprovable, "SZS status: CounterSatisfiable"),