# HG changeset patch
# User blanchet
# Date 1406280379 -7200
# Node ID 6be7551476955ff2b4acca83429c265a0e71ceb7
# Parent  dc5e1b1db9ba84db31b21858297e3277a06d81ce
tuning

diff -r dc5e1b1db9ba -r 6be755147695 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 25 11:26:17 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 25 11:26:19 2014 +0200
@@ -261,9 +261,9 @@
      |> implode) ^
     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
-    \FIFOWeight(PreferProcessed))'"
+    \FIFOWeight(PreferProcessed))' "
   else
-    "-xAuto"
+    "-xAuto "
 
 val e_ord_weights =
   map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
@@ -273,10 +273,8 @@
 fun e_term_order_info_arguments false false _ = ""
   | e_term_order_info_arguments gen_weights gen_prec ord_info =
     let val ord_info = ord_info () in
-      (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' "
-       else "") ^
-      (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' "
-       else "")
+      (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^
+      (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
     end
 
 val e_config : atp_config =
@@ -287,8 +285,8 @@
      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 ^ " " ^
+       e_selection_weight_arguments ctxt heuristic sel_weights ^
+       e_term_order_info_arguments gen_weights gen_prec ord_info ^
        "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
        (if full_proofs orelse not (is_e_at_least_1_8 ()) then