# HG changeset patch
# User blanchet
# Date 1400535833 -7200
# Node ID 10f68b83b474ea3cc7f7d02cdc3fe6d47829416e
# Parent  d3eed0518882b6de98449a579a295acd19367c8b
use E 1.8's auto scheduler option

diff -r d3eed0518882 -r 10f68b83b474 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 19 23:43:53 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 19 23:43:53 2014 +0200
@@ -338,10 +338,10 @@
 
 val e_config : atp_config =
   {exec = (fn () => (["E_HOME"],
-       if is_e_at_least_1_8 () then ["eprover"] else ["eproof_ram", "eproof"])),
-   arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout =>
-       fn file_name =>
-       fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
+     if is_e_at_least_1_8 () then ["eprover"] else ["eproof_ram", "eproof"])),
+   arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => fn file_name =>
+     fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
+       (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
        "--tstp-in --tstp-out --silent " ^
        e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
        e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
@@ -351,10 +351,8 @@
           " --proof-object=1"
         else
           " --output-level=5" ^
-          (if is_e_at_least_1_6 () then
-             " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
-           else
-             "")) ^
+          (if is_e_at_least_1_6 () then " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
+           else "")) ^
        " " ^ file_name,
    proof_delims =
      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @